supDegree_mul_of_ne_zero_left — Mathlib

English

If D is injective and additive, and the left factor p is nonzero while q is monic with respect to D, then supDegree_D(p q) = supDegree_D(p) + supDegree_D(q).

Русский

Если D инъективна и аддитивна, и левая часть p непустая, а правая часть q монична относительно D, то supDegree_D(p q) = supDegree_D(p) + supDegree_D(q).

LaTeX

$$$$\operatorname{supDegree}_D(p q) = \operatorname{supDegree}_D(p) + \operatorname{supDegree}_D(q)$$$$

Lean4

theorem supDegree_mul_of_ne_zero_left (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hq : q.Monic D)
    (hp : p ≠ 0) : (p * q).supDegree D = p.supDegree D + q.supDegree D :=
  by
  cases subsingleton_or_nontrivial R; · exact (hp (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp hq.ne_zero
  simp_rw [hq, mul_one, Ne, leadingCoeff_eq_zero hD, hp, not_false_eq_true]

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