of_dvd_add — Mathlib

English

If b divides a + r and deg r < m with n ≤ m, and a is monic of degree m, b monic of degree n, then there exists q monic of degree m − n with a = q b − r.

Русский

Если b делит a + r и deg r < m, и a моноичен степени m, b моноичен степени n, то существует моноичный q степени m − n такой, что a = q b − r.

LaTeX

$$$\\exists q:\\\,R[X],\\ IsMonicOfDegree\\!q\\ (m-n) \\land a = q \\cdot b - r$$$

Lean4

theorem of_dvd_add {a b r : R[X]} {m n : ℕ} (hmn : n ≤ m) (ha : IsMonicOfDegree a m) (hb : IsMonicOfDegree b n)
    (hr : r.natDegree < m) (h : b ∣ a + r) : ∃ q : R[X], IsMonicOfDegree q (m - n) ∧ a = q * b - r :=
  by
  obtain ⟨q, hq⟩ := exists_eq_mul_left_of_dvd h
  refine ⟨q, hb.of_mul_right ?_, eq_sub_iff_add_eq.mpr hq⟩
  rw [← hq, show m - n + n = m by cutsat]
  exact ha.add_right hr

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