roots_multiset_prod_X_sub_C — Mathlib

English

Let R be a commutative domain. For any finite multiset s of elements of R, the polynomial P(X) = ∏_{a ∈ s} (X − a) has as its roots exactly the elements of s, counted with multiplicity.

Русский

Пусть R — коммутативное интегральное кольцо. Для любой конечной мультимножества s элементов R полином P(X) = ∏_{a ∈ s} (X − a) имеет корнями ровно элементы s с учётом кратностей.

LaTeX

$$$\operatorname{roots}\left(\prod_{a \in s} (X - C a)\right) = s$$$

Lean4

@[simp]
theorem roots_multiset_prod_X_sub_C (s : Multiset R) : (s.map fun a => X - C a).prod.roots = s :=
  by
  rw [roots_multiset_prod, Multiset.bind_map]
  · simp_rw [roots_X_sub_C]
    rw [Multiset.bind_singleton, Multiset.map_id']
  · rw [Multiset.mem_map]
    rintro ⟨a, -, h⟩
    exact X_sub_C_ne_zero a h

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