carrier_eq_mk_aroots_minpoly — Mathlib

English

The carrier is equal to the mk-aroots-minpoly representation: c.carrier.toFinset = ⟨c.minpoly.aroots L, c.nodup_aroots_minpoly⟩.

Русский

Носитель равен представлению mk-aroots-minpoly: c.carrier.toFinset равен ⟨c.minpoly.aroots L, c.nodup_aroots_minpoly⟩.

LaTeX

$$$ c.carrier.toFinset = \\langle c.minpoly.aroots L, c.nodup_aroots_minpoly \\rangle $$$

Lean4

theorem carrier_eq_mk_aroots_minpoly (c : ConjRootClass K L) [Fintype c.carrier] :
    c.carrier.toFinset = ⟨c.minpoly.aroots L, c.nodup_aroots_minpoly⟩ := by simp only [aroots_minpoly_eq_carrier_val]

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