map_normEDS — Mathlib

English

Let f : R →+* S be a ring hom between commutative rings and b, c, d ∈ R. Then f(normEDS(b,c,d,n)) = normEDS(f(b), f(c), f(d), n) for all n ∈ ℤ.

Русский

Пусть f: R →+* S — кольцевой гомоморфизм между коммутативными кольцами и b, c, d ∈ R. Тогда f(normEDS(b,c,d,n)) = normEDS(f(b), f(c), f(d), n) для всех n ∈ ℤ.

LaTeX

$$$\\forall b,c,d\\in R\\,\\forall n\\in\\mathbb Z:\\ f(\\mathrm{normEDS}(b,c,d,n))=\\mathrm{normEDS}(f(b),f(c),f(d),n).$$$

Lean4

@[simp]
theorem map_normEDS (n : ℤ) : f (normEDS b c d n) = normEDS (f b) (f c) (f d) n := by simp [normEDS, apply_ite f]

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