Theorem: MvPolynomial.rTensorAlgHom_apply_eq (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
p : MvPolynomial σ S ⊗[R] N
⊢ rTensorAlgHom p = (finsuppLeft' R S N (σ →₀ ℕ) S) p
Tactic:
rw [← AlgHom.toLinearMap_apply, 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
p : MvPolynomial σ S ⊗[R] N
⊢ ↑(finsuppLeft' R S N (σ →₀ ℕ) S) p = (finsuppLeft' R S N (σ →₀ ℕ) S) p

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
p : MvPolynomial σ S ⊗[R] N
⊢ ↑(finsuppLeft' R S N (σ →₀ ℕ) S) p = (finsuppLeft' R S N (σ →₀ ℕ) S) p
Tactic:
rfl
State after:
no goals