degree_prod — Mathlib

English

For a finite set s of polynomials f_i ∈ R[X], deg(∏_{i∈s} f_i) = ∑_{i∈s} deg(f_i) provided each f_i is nonzero.

Русский

Пусть s конечное множество полиномов; степень произведения равна сумме степеней, если все полиномы непустые.

LaTeX

$$$$\left( \forall i\in s, \ f_i \neq 0 \right) \implies \operatorname{degree}\left( \prod_{i\in s} f_i \right) = \sum_{i\in s} \operatorname{degree}(f_i).$$$$

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_prod [Nontrivial R] : (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree :=
  map_prod (@degreeMonoidHom R _ _ _) _ _

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