English
If D is injective and additive, and p and q are nonzero 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 (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hbot : (⊥ : B) + ⊥ = ⊥)
(hp : p.Monic D) (hq : q.Monic D) : (p * q).supDegree D = p.supDegree D + q.supDegree D :=
by
cases subsingleton_or_nontrivial R
· simp_rw [Subsingleton.eq_zero p, Subsingleton.eq_zero q, mul_zero, supDegree_zero, hbot]
exact hq.supDegree_mul_of_ne_zero_left hD hadd hp.ne_zero
