English
Let f: σ → τ be a function on index sets and p a natural number. Then the two algebra homomorphisms from MvPolynomial σ R to MvPolynomial τ R obtained by first renaming by f and then expanding by p, and by first expanding by p and then renaming by f, are equal.
Русский
Пусть f: σ → τ и p ∈ ℕ. Тогда два алгебраических гомоморфизма из MvPolynomial σ R в MvPolynomial τ R, полученные последовательностями переименования по f затем расширения на p и расширения на p затем переименования по f, совпадают.
LaTeX
$$$(\\text{rename } f) \\circ (\\text{expand } p) = (\\text{expand } p) \\circ (\\text{rename } f : \\operatorname{MvPolynomial} \\sigma R \\to \\operatorname{MvPolynomial} \\tau R)$$$
Lean4
@[simp]
theorem rename_comp_expand (f : σ → τ) (p : ℕ) :
(rename f).comp (expand p) = (expand p).comp (rename f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R) :=
by
ext1 φ
simp only [rename_expand, AlgHom.comp_apply]
