mod_eq_self_iff — Mathlib

English

If q ≠ 0, then p % q = p if and only if deg p < deg q.

Русский

Если q ≠ 0, то p % q = p тогда и только тогда, когда deg p < deg q.

LaTeX

$$$ p \bmod q = p \iff \deg p < \deg q \qquad( q \neq 0 )$$$

Lean4

theorem mod_eq_self_iff (hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q :=
  ⟨fun h => h ▸ EuclideanDomain.mod_lt _ hq0, fun h => by
    classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p := not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]⟩

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