degree_div_lt — Mathlib

English

If p ≠ 0 and deg q > 0, then deg(p/q) < deg p.

Русский

Если p ≠ 0 и deg q > 0, то deg(p/q) < deg p.

LaTeX

$$$ \deg\left(\frac{p}{q}\right) < \deg p \quad \text{если } p \neq 0\text{ и }0 < \deg q$$$

Lean4

theorem degree_div_lt (hp : p ≠ 0) (hq : 0 < degree q) : degree (p / q) < degree p :=
  by
  have hq0 : q ≠ 0 := fun hq0 => by simp [hq0] at hq
  rw [div_def, mul_comm, degree_mul_leadingCoeff_inv _ hq0]
  exact degree_divByMonic_lt _ (monic_mul_leadingCoeff_inv hq0) hp (by rw [degree_mul_leadingCoeff_inv _ hq0]; exact hq)

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