mod_add — Mathlib

English

If f and f' are power series, then H.div (f + f') = H.div f + H.div f'.

Русский

Для степенных рядов из f и f' выполняется: H.div (f + f') = H.div f + H.div f'.

LaTeX

$$$ \\mathrm{div}(f+f') = \\mathrm{div}(f) + \\mathrm{div}(f'). $$$

Lean4

@[simp]
theorem mod_add [IsAdicComplete I A] : H.mod (f + f') = H.mod f + H.mod f' :=
  by
  have H1 := (H.isWeierstrassDivisionAt_div_mod f).add (H.isWeierstrassDivisionAt_div_mod f')
  have H2 := H.isWeierstrassDivisionAt_div_mod (f + f')
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

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