degree_add_div — Mathlib

English

Same as degree_add_div: deg q + deg(p/q) = deg p under q ≠ 0 and deg q ≤ deg p.

Русский

То же, что и ранее: deg q + deg(p/q) = deg p при q ≠ 0 и deg q ≤ deg p.

LaTeX

$$$ \deg q + \deg\left(\frac{p}{q}\right) = \deg p \quad (q \neq 0,\ deg q \le \deg p) $$$

Lean4

theorem degree_add_div (hq0 : q ≠ 0) (hpq : degree q ≤ degree p) : degree q + degree (p / q) = degree p :=
  by
  have : degree (p % q) < degree (q * (p / q)) :=
    calc
      degree (p % q) < degree q := EuclideanDomain.mod_lt _ hq0
      _ ≤ _ := degree_le_mul_left _ (mt (Polynomial.div_eq_zero_iff hq0).1 (not_lt_of_ge hpq))
  conv_rhs => rw [← EuclideanDomain.div_add_mod p q, degree_add_eq_left_of_degree_lt this, degree_mul]

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