map_rename — Mathlib

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]

Похожие утверждения