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

State before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R rTensorAlgHom.toLinearMap = ↑(finsuppLeft R S N (σ →₀ ℕ))
Tactic:
rw [rTensorAlgHom_toLinearMap]
State after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R ↑(finsuppLeft' R S N (σ →₀ ℕ) S) = ↑(finsuppLeft R S N (σ →₀ ℕ))

State before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ ↑R ↑(finsuppLeft' R S N (σ →₀ ℕ) S) = ↑(finsuppLeft R S N (σ →₀ ℕ))
Tactic:
rfl
State after:
no goals