supDegree_mul — Mathlib

English

Under the same injectivity and additivity assumptions on D, the supDegree is additive over multiplication: supDegree_D(p q) = supDegree_D(p) + supDegree_D(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)
    (hpq : leadingCoeff D p * leadingCoeff D q ≠ 0) (hp : p ≠ 0) (hq : q ≠ 0) :
    (p * q).supDegree D = p.supDegree D + q.supDegree D :=
  by
  apply supDegree_eq_of_max
  · rw [← AddSubsemigroup.coe_set_mk (Set.range D), ← AddHom.srange_mk _ hadd, SetLike.mem_coe]
    · exact add_mem (supDegree_mem_range D hp) (supDegree_mem_range D hq)
    · exact (AddHom.srange ⟨D, hadd⟩).add_mem
  · simp_rw [Finsupp.mem_support_iff, apply_supDegree_add_supDegree hD hadd]
    exact hpq
  · have := addLeftMono_of_addLeftStrictMono B
    have := addRightMono_of_addRightStrictMono B
    exact fun a ha => (Finset.le_sup ha).trans (supDegree_mul_le hadd)

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