divByMonic_eq_zero_iff — Mathlib

English

For monic q, p /ₘ q = 0 iff deg p < deg q.

Русский

Для монического q, p /ₘ q = 0 тогда и только тогда, когда deg p < deg q.

LaTeX

$$$ p /_{m} q = 0 \iff \deg p < \deg q \quad (\operatorname{Monic}(q)) $$$

Lean4

theorem divByMonic_eq_zero_iff [Nontrivial R] (hq : Monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
  ⟨fun h => by
    have := modByMonic_add_div p hq
    rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this, fun h => by
    classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩

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