map_complEDS — Mathlib

English

Let f : R →+* S be a ring hom and b, c, d ∈ R. Then f(complEDS(b,c,d,k,n)) = complEDS(f(b),f(c),f(d),k,n) for all k ∈ ℤ and n ∈ ℤ, i.e. f preserves the EDS construction with parameters.

Русский

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

LaTeX

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

Lean4

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

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