natDegree_multiset_prod_of_monic — Mathlib

English

Let t be a multiset of polynomials in R[X], and assume every element is monic. Then natDegree(t.prod) = (t.map natDegree).sum.

Русский

Пусть t — мультисет многочленов над R; каждый элемент моничен. Тогда natDegree(t.prod) равно сумме natDegree каждого элемента.

LaTeX

$$$$\left(\forall f \in t, \operatorname{Monic}(f)\right) \implies \operatorname{natDegree}\left( t.prod \right) = \sum_{f \in t} \operatorname{natDegree}(f).$$$$

Lean4

theorem natDegree_multiset_prod_of_monic (h : ∀ f ∈ t, Monic f) : t.prod.natDegree = (t.map natDegree).sum :=
  by
  nontriviality R
  apply natDegree_multiset_prod'
  simp_all

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