minpoly_inj

Mathlib.FieldTheory.Minpoly.ConjRootClass

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

English

The map c ↦ c.minpoly is injective: if c.minpoly = d.minpoly, then c = d.

Русский

Отображение c ⟼ c.minpoly инъективно: если c.minpoly = d.minpoly, то c = d.

LaTeX

$$$\\forall c,d: (c.minpoly = d.minpoly) \\Rightarrow (c = d)$$$

Lean4

@[simp]
theorem minpoly_inj {c d : ConjRootClass K L} : c.minpoly = d.minpoly ↔ c = d :=
  by
  induction c
  induction d
  simp [isConjRoot_def]

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

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

Разделы

Аффилиация

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