Theorem: MonoidAlgebra.rTensorAlgHom_toLinearMap' (DividedPowers/ForMathlib/RingTheory/TensorProduct/MonoidAlgebra.lean)

State before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft R M N α)
Tactic:
rw [rTensorAlgHom_toLinearMap]
State after:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ ↑(finsuppLeft' R M N α R) = ↑(finsuppLeft R M N α)

State before:
α : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst✝¹⁰ : Monoid α
inst✝⁹ : DecidableEq α
inst✝⁸ : CommSemiring R
S : Type u_6
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
inst✝⁵ : Semiring M
inst✝⁴ : Algebra R M
inst✝³ : Algebra S M
inst✝² : IsScalarTower R S M
inst✝¹ : Semiring N
inst✝ : Algebra R N
⊢ ↑(finsuppLeft' R M N α R) = ↑(finsuppLeft R M N α)
Tactic:
rfl
State after:
no goals