English
For a ring hom f : R →+* S and parameters k ∈ ℤ, n ∈ ℕ, we have f(complEDS'(b,c,d,k,n)) = complEDS'(f(b), f(c), f(d), k, n).
Русский
Для кольцевого гомоморфизма f: R →+* S и параметров k ∈ ℤ, n ∈ ℕ выполняется f(complEDS'(b,c,d,k,n)) = complEDS'(f(b), f(c), f(d), k, n).
LaTeX
$$$\\forall b,c,d\\in R\\,\\forall k\\in\\mathbb Z\\,\\forall n\\in\\mathbb N:\\ 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
induction n using complEDSRec' with
| zero => simp
| one => simp
| _ _ ih =>
simp only [complEDS'_even, complEDS'_odd, map_normEDS, map_complEDS₂, map_pow, map_mul, map_sub]
repeat rw [ih _ <| by linarith only]
