decidable

Mathlib.FieldTheory.Minpoly.IsConjRoot

URI: https://scilib.ai/kg/mathlib#IsConjRoot.decidable

Lean4

instance decidable [Normal K L] [DecidableEq L] [Fintype (L ≃ₐ[K] L)] (x y : L) : Decidable (IsConjRoot K x y) :=
  decidable_of_iff _ isConjRoot_iff_exists_algEquiv.symm

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

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

Разделы

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

Аффилиация

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