Theorem: PolynomialMap.ofLinearMap_mem_grade_one (DividedPowers/PolynomialMap/Homogeneous.lean)

State before:
R : Type u
inst✝⁴ : CommRing R
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
v : M →ₗ[R] N
S : Type u
x✝¹ : CommRing S
x✝ : Algebra R S
r : S
m : S ⊗[R] M
⊢ (ofLinearMap v).toFun' S (r • m) = r ^ 1 • (ofLinearMap v).toFun' S m
Tactic:
simp only [ofLinearMap, LinearMapClass.map_smul, pow_one]
State after:
no goals