div_add — Mathlib

English

Again, q_0 = 0 holds for the Weierstrass quotient sequence.

Русский

Снова имеем q_0 = 0 для последовательности делителя Вейершстра.

LaTeX

$$$ H.seq f 0 = 0. $$$

Lean4

@[simp]
theorem div_add [IsAdicComplete I A] : H.div (f + f') = H.div f + H.div 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)).1

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