degree_list_prod — Mathlib

English

Let t be a multiset of polynomials with 0 ∉ t. Then natDegree t.prod = (t.map natDegree).sum.

Русский

Пусть t — мультимножество полиномов без нулевого элемента; тогда natDegree произведения равно сумме natDegree всех элементов.

LaTeX

$$$$\operatorname{natDegree}(t.prod) = \sum_{p\in t} \operatorname{natDegree}(p) \,\text{when } 0 \notin t.$$$$

Lean4

/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
`[Nontrivial R]` is needed, otherwise for `l = []` we have `⊥` in the LHS and `0` in the RHS.
-/
theorem degree_list_prod [Nontrivial R] (l : List R[X]) : l.prod.degree = (l.map degree).sum :=
  map_list_prod (@degreeMonoidHom R _ _ _) l

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