map_preNormEDS' — Mathlib

English

Let f be a ring homomorphism. Then it commutes with the preNormEDS' construction:

Русский

Пусть f — гомоморфизм колец. Тогда он сохраняет конструкцию preNormEDS':

LaTeX

$$$f\bigl(\\mathrm{preNormEDS}'(b,c,d,n)\\bigr) = \\mathrm{preNormEDS}'(f(b), f(c), f(d), n) \\text{ for all } n \in \mathbb{N}$$$

Lean4

@[simp]
theorem map_preNormEDS' (n : ℕ) : f (preNormEDS' b c d n) = preNormEDS' (f b) (f c) (f d) n := by
  induction n using normEDSRec' with
  | zero => simp
  | one => simp
  | two => simp
  | three => simp
  | four => simp
  | _ _ ih =>
    simp only [preNormEDS'_even, preNormEDS'_odd, apply_ite f, map_pow, map_mul, map_sub, map_one]
    repeat rw [ih _ <| by linarith only]

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