degree_multiset_prod — Mathlib

English

The degree of a product over a multiset equals the sum of the degrees of the factors, i.e., deg(t.prod) = ∑ deg(p) for p ∈ t, when t is a multiset of polynomials.

Русский

Степень произведения по мультисету равна сумме степеней множителей.

LaTeX

$$$$\operatorname{degree}(t.prod) = \sum_{p\in t} \operatorname{degree}(p).$$$$

Lean4

/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
-/
theorem degree_multiset_prod [Nontrivial R] : t.prod.degree = (t.map fun f => degree f).sum :=
  map_multiset_prod (@degreeMonoidHom R _ _ _) _

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