supDegree_mul_of_ne_zero_right — Mathlib

English

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

Русский

Если D инъективна и аддитивна, и правая часть q непустая, а левая часть p моничная относительно 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_right (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hp : p.Monic D)
    (hq : q ≠ 0) : (p * q).supDegree D = p.supDegree D + q.supDegree D :=
  by
  cases subsingleton_or_nontrivial R; · exact (hq (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp.ne_zero hq
  simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]

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