English
For any n and x, the equivalence sends singleton to monomial: equivPolynomial (single R n x) = monomial n x.
Русский
Эквивелентность отображает одинокий элемент в моном: equivPolynomial (single R n x) = monomial n x.
LaTeX
$$equivPolynomial (single R n x) = monomial n x$$
Lean4
theorem map_smul (f : M →ₗ[R] M') (p : R[X]) (q : PolynomialModule R M) :
map R' f (p • q) = p.map (algebraMap R R') • map R' f q := by
induction q using induction_linear with
| zero => rw [smul_zero, map_zero, smul_zero]
| add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
| single i m =>
induction p using Polynomial.induction_on' with
| add _ _ e₁ e₂ => rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
| monomial =>
rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single, monomial_smul_single, f.map_smul,
algebraMap_smul]
