map_complEDS₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem map_complEDS₂ (n : ℤ) : f (complEDS₂ b c d n) = complEDS₂ (f b) (f c) (f d) n := by
  simp [complEDS₂, apply_ite f]

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