instEuclideanDomain — Mathlib

English

For polynomials p and q over a field with q ≠ 0 and deg q ≤ deg p, we have deg q + deg(p/q) = deg p.

Русский

Для многочленов p и q над полеc с q ≠ 0 и deg q ≤ deg p выполняется deg q + deg(p/q) = deg p.

LaTeX

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

Lean4

instance instEuclideanDomain : EuclideanDomain R[X] :=
  { Polynomial.commRing, Polynomial.nontrivial with
    quotient := (· / ·)
    quotient_zero := by simp [div_def]
    remainder := (· % ·)
    r := _
    r_wellFounded := degree_lt_wf
    quotient_mul_add_remainder_eq := quotient_mul_add_remainder_eq_aux
    remainder_lt := fun _ _ hq => remainder_lt_aux _ hq
    mul_left_not_lt := fun _ _ hq => not_lt_of_ge (degree_le_mul_left _ hq) }

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