natDegree_finset_prod_X_sub_C_eq_card

English

For a finite set s and function f: α → R, natDegree of ∏_{a∈s} (X − C(f a)) equals card(s).

Русский

Для конечного множества s и функции f полиномов natDegree произведения ∏_{a∈s} (X − C(f a)) равен card(s).

LaTeX

$$$$\operatorname{natDegree}\left(\prod_{a\in s} (X - C(f(a)))\right) = |s|.$$$$

Lean4

@[simp]
theorem natDegree_finset_prod_X_sub_C_eq_card {α} (s : Finset α) (f : α → R) :
    (∏ a ∈ s, (X - C (f a))).natDegree = s.card := by
  rw [Finset.prod, ← (X - C ·).comp_def f, ← Multiset.map_map, natDegree_multiset_prod_X_sub_C_eq_card,
    Multiset.card_map, Finset.card]

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