map_comp_rename — Mathlib

English

For ring Hom f: R →+* S and g: σ → τ, the composed maps satisfy (map f) ∘ (rename g) = (rename g) ∘ (map f).

Русский

Для гомоморфизма колец f: R →+* S и отображения g: σ → τ выполняется (map f) ∘ (rename g) = (rename g) ∘ (map f).

LaTeX

$$$(\\text{map } f) \\circ (\\text{rename } g) = (\\text{rename } g) \\circ (\\text{map } f).$$$

Lean4

theorem map_comp_rename (f : R →+* S) (g : σ → τ) :
    (map f).comp (rename g).toRingHom = (rename g).toRingHom.comp (map f) :=
  RingHom.ext fun p ↦ map_rename f g p

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