roots_prod_X_sub_C — Mathlib

English

Let s be a finite set of elements of R. Then the roots of the product over a ∈ s of (X − C a) are exactly the elements of s.

Русский

Пусть s — конечное множество элементов R. Тогда корни произведения по a ∈ s (X − C a) равны точно элементам s.

LaTeX

$$$ (s.prod\ fun a => X - C\ a).roots = s.val $$$

Lean4

theorem roots_prod_X_sub_C (s : Finset R) : (s.prod fun a => X - C a).roots = s.val :=
  by
  apply (roots_prod (fun a => X - C a) s ?_).trans
  · simp_rw [roots_X_sub_C]
    rw [Multiset.bind_singleton, Multiset.map_id']
  · refine prod_ne_zero_iff.mpr (fun a _ => X_sub_C_ne_zero a)

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