aroots_minpoly_eq_carrier_val — Mathlib

English

If c is separable and finite, the roots of c.minpoly over L coincide with the carrier elements: aroots_minpoly_eq_carrier_val.

Русский

Если c разделим и конечен, корни c.minpoly над L совпадают с элементами носителя.

LaTeX

$$$ c.minpoly.aroots L = c.carrier.Elem$$$

Lean4

theorem aroots_minpoly_eq_carrier_val (c : ConjRootClass K L) [Fintype c.carrier] :
    c.minpoly.aroots L = c.carrier.toFinset.1 := by
  classical
    simp_rw [← rootSet_minpoly_eq_carrier, rootSet_def, Finset.toFinset_coe, Multiset.toFinset_val,
    c.nodup_aroots_minpoly.dedup]

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