English
Let R and S be commutative rings and f : R →+* S a ring hom. Then for all b, c, d ∈ R and all integers n, the preNormEDS construction commutes with f, i.e. f(preNormEDS(b, c, d, n)) = preNormEDS(f(b), f(c), f(d), n).
Русский
Пусть R и S — коммутативные кольца, а f: R →+* S — кольцевой гомоморфизм. Тогда для любых b, c, d ∈ R и любых целых n конструкция preNormEDS сохраняется под F, то есть f(preNormEDS(b, c, d, n)) = preNormEDS(f(b), f(c), f(d), n).
LaTeX
$$$\\forall b,c,d\\in R\\,\\forall n\\in\\mathbb Z:\\ f\\bigl(\\mathrm{preNormEDS}(b,c,d,n)\\bigr)=\\mathrm{preNormEDS}\\bigl(f(b),f(c),f(d),n\\bigr).$$$
Lean4
@[simp]
theorem map_preNormEDS (n : ℤ) : f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n := by simp [preNormEDS]
