sub_of_right — Mathlib

English

If q.leadingCoeff = -1 and degree(p) < degree(q), then p − q is monic.

Русский

Если q.leadingCoeff = -1 и deg p < deg q, то p − q мононичен.

LaTeX

$$$\forall {R} [\text{Ring } R] {p q : Polynomial R}, q.leadingCoeff = -1 \rightarrow degree p < degree q \rightarrow (p - q).Monic$$$

Lean4

theorem sub_of_right {p q : R[X]} (hq : q.leadingCoeff = -1) (hpq : degree p < degree q) : Monic (p - q) :=
  by
  have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
  rw [sub_eq_add_neg]
  apply Monic.add_of_right this
  rwa [degree_neg]

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