nodup_aroots_minpoly

Mathlib.FieldTheory.Minpoly.ConjRootClass

URI: https://scilib.ai/kg/mathlib#ConjRootClass.nodup_aroots_minpoly

English

Under separability, the roots of c.minpoly in L are nodal (no repeats): (c.minpoly.aroots L).Nodup.

Русский

При разделимости корни c.minpoly в L не повторяются: (c.minpoly.aroots L).Nodup.

LaTeX

$$$ (c.minpoly.aroots L).\\mathrm{Nodup}$$$

Lean4

theorem nodup_aroots_minpoly (c : ConjRootClass K L) : (c.minpoly.aroots L).Nodup :=
  nodup_roots c.separable_minpoly.map

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru