add — Mathlib

English

If f and f' satisfy Weierstrass division conditions with respective g, q, r and q', r', then f+f' satisfies with g and q+q', r+r'.

Русский

Если f и f' удовлетворяют условиям деления Вайершстраса, то сумма удовлетворяет для сумм г, q и r.

LaTeX

$$$\\forall {f,g,q,r,I,f',q',r'}(H : f.IsWeierstrassDivisionAt g q r I) (H' : f'.IsWeierstrassDivisionAt g q' r' I), \\; (f+f').IsWeierstrassDivisionAt g (q+q') (r+r') I$$$

Lean4

theorem add {f' q' r'} (H : f.IsWeierstrassDivisionAt g q r I) (H' : f'.IsWeierstrassDivisionAt g q' r' I) :
    (f + f').IsWeierstrassDivisionAt g (q + q') (r + r') I :=
  ⟨(Polynomial.degree_add_le _ _).trans_lt (sup_lt_iff.2 ⟨H.degree_lt, H'.degree_lt⟩), by
    rw [H.eq_mul_add, H'.eq_mul_add, Polynomial.coe_add]; ring⟩

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