div_eq_zero_iff — Mathlib

English

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

Русский

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

LaTeX

$$$ \frac{p}{q} = 0 \iff \deg p < \deg q \quad (q \neq 0)$$$

Lean4

protected theorem div_eq_zero_iff (hq0 : q ≠ 0) : p / q = 0 ↔ degree p < degree q :=
  ⟨fun h => by
    have := EuclideanDomain.div_add_mod p q
    rwa [h, mul_zero, zero_add, mod_eq_self_iff hq0] at this, fun h =>
    by
    have hlt : degree p < degree (q * C (leadingCoeff q)⁻¹) := by rwa [degree_mul_leadingCoeff_inv q hq0]
    have hm : Monic (q * C (leadingCoeff q)⁻¹) := monic_mul_leadingCoeff_inv hq0
    rw [div_def, (divByMonic_eq_zero_iff hm).2 hlt, mul_zero]⟩

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