add_weierstrassDiv — Mathlib

English

Weierstrass division distributes over addition: the quotient of f+f' by g is the sum of quotients, and the remainder is additive as well.

Русский

Деление по Вайершстрасу совместимо с сложением: частное (f+f')/ʷg = f/ʷg + f'/ʷg, остаток аналогично.

LaTeX

$$$((f+f')/ʷ g) = (f/ʷ g) + (f'/ʷ g)$$$

Lean4

@[simp]
theorem add_weierstrassDiv [IsAdicComplete (IsLocalRing.maximalIdeal A) A] : (f + f') /ʷ g = f /ʷ g + f' /ʷ g :=
  by
  simp_rw [weierstrassDiv]
  split_ifs <;> simp

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