nodup_roots

Mathlib.FieldTheory.Separable

URI: https://scilib.ai/kg/mathlib#Polynomial.nodup_roots

← MathLib Explorer

English

If p is separable, then the multiset of its roots is without repetition.

Русский

Если p сепарабелен, то моносет его корней без повторений.

LaTeX

$$$ p.Separable \Rightarrow p.roots.Nodup$$$

Lean4

theorem nodup_roots {p : R[X]} (hsep : Separable p) : p.roots.Nodup := by
  classical exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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