English
Let f: R →+* S be a ring hom and g: σ → τ. For any p in MvPolynomial σ R, map f (rename g p) = rename g (map f p).
Русский
Пусть f: R →+* S — гомоморфизм колец и g: σ → τ. Для любого p ∈ MvPolynomial σ R выполняется map f (rename g p) = rename g (map f p).
LaTeX
$$$\\text{map } f (\\text{rename } g \\, p) = \\text{rename } g\\, (\\text{map } f\\, p).$$$
Lean4
theorem map_rename (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R) : map f (rename g p) = rename g (map f p) := by
apply
MvPolynomial.induction_on p (fun a => by simp only [map_C, rename_C])
(fun p q hp hq => by simp only [hp, hq, map_add]) fun p n hp => by simp only [hp, rename_X, map_X, map_mul]