leadingCoeff_mul_eq_left — 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 leadingCoeff_mul_eq_left (hD : D.Injective) (hadd : ∀ a1 a2, D (a1 + a2) = D a1 + D a2) (hq : q.Monic D) :
    (p * q).leadingCoeff D = p.leadingCoeff D :=
  by
  obtain rfl | hp := eq_or_ne p 0
  · rw [zero_mul]
  rw [leadingCoeff, hq.supDegree_mul_of_ne_zero_left hD hadd hp, apply_supDegree_add_supDegree hD hadd, hq, mul_one]

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