mul — Mathlib

English

If p and q are monic with respect to D, then (p q).supDegree D = p.supDegree D + q.supDegree D.

Русский

Если p и q моничны по D, то (p q).supDegree D = p.supDegree D + q.supDegree D.

LaTeX

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

Lean4

theorem mul (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hp : p.Monic D) (hq : q.Monic D) :
    (p * q).Monic D := by rw [Monic, hq.leadingCoeff_mul_eq_left hD hadd]; exact hp

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