English
There is a scalar-tower S over R[X] acting on PolynomialModule R M; associativity of smul holds in this tower.
Русский
Существует башня скаляров S над R[X], действующая на PolynomialModule R M; выполняется ассоциативность скаляров.
LaTeX
$$IsScalarTower S (Polynomial R) (PolynomialModule R M)$$
Lean4
@[simp]
theorem monomial_smul_single (i : ℕ) (r : R) (j : ℕ) (m : M) : monomial i r • single R j m = single R (i + j) (r • m) :=
by
simp only [Module.End.mul_apply, Polynomial.aeval_monomial, Module.End.pow_apply, Module.algebraMap_end_apply,
smul_def]
induction i generalizing r j m with
| zero =>
rw [Function.iterate_zero, zero_add]
exact Finsupp.smul_single r j m
| succ n hn =>
rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
congr 2
rw [Nat.one_add]
exact Finsupp.mapDomain_single
