Theorem: Polynomial.rTensorAlgHom_apply_eq (DividedPowers/ForMathlib/RingTheory/TensorProduct/Polynomial.lean)

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ (rTensorAlgHom R N S) p = (rTensorLinearEquiv R N S) p
Tactic:
rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
State after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ ↑(rTensorLinearEquiv R N S) p = (rTensorLinearEquiv R N S) p

State before:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : CommSemiring N
inst✝² : Algebra R N
S : Type u_4
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
p : S[X] ⊗[R] N
⊢ ↑(rTensorLinearEquiv R N S) p = (rTensorLinearEquiv R N S) p
Tactic:
rfl
State after:
no goals