degree_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 degree(∏_{i∈s} f_i) = ∑_{i∈s} degree(f_i).

Русский

Пусть s — конечное множество; каждый f_i моничен. Тогда deg(∏ f_i) = ∑ deg(f_i).

LaTeX

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

Lean4

theorem degree_prod_of_monic [Nontrivial R] (h : ∀ i ∈ s, (f i).Monic) :
    (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree := by
  simpa using degree_multiset_prod_of_monic (s.1.map f) (by simpa using h)

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