Theorem: LinearForm.baseChange_apply_tmul (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : M →ₗ[R] R
r : S
m : M
⊢ (baseChange R S M f) (r ⊗ₜ[R] m) = r * f m • 1
Tactic:
simp only [baseChange, coe_comp, Function.comp_apply, baseChange_tmul,
  AlgHom.toLinearMap_apply, rid'_tmul, Algebra.mul_smul_comm, _root_.mul_one]
State after:
no goals