natDegree_prod_of_monic — Mathlib

English

Let s be a finite set and f_i ∈ R[X] with (f_i) monic for all i ∈ s. Then natDegree(∏_{i∈s} f_i) = ∑_{i∈s} natDegree(f_i).

Русский

Пусть s — конечное множество; для каждого i ∈ s полином f_i ∈ R[X] моничен. Тогда natDegree произведения равен сумме natDegree каждого f_i.

LaTeX

$$$$\left( \forall i \in s, \ (f(i)).Monic \right) \implies \operatorname{natDegree}\left( \prod_{i\in s} f(i) \right) = \sum_{i\in s} \operatorname{natDegree}(f(i)).$$$$

Lean4

theorem natDegree_prod_of_monic (h : ∀ i ∈ s, (f i).Monic) : (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree := by
  simpa using natDegree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

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