modByMonic_eq_self_iff — Mathlib

English

For any p and monic q, p %ₘ q = p if and only if deg p < deg q.

Русский

Для любых p и монического q: p %ₘ q = p тогда и только тогда, когда deg p < deg q.

LaTeX

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

Lean4

theorem modByMonic_eq_self_iff [Nontrivial R] (hq : Monic q) : p %ₘ q = p ↔ degree p < degree q :=
  ⟨fun h => h ▸ degree_modByMonic_lt _ hq, fun h => by
    classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold modByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩

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