ConjRootClass

Mathlib.FieldTheory.Minpoly.ConjRootClass

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

English

ConjRootClass K L is the quotient of L by the relation IsConjRoot K L.

Русский

ConjRootClass K L есть фактор-морфизм L по отношению IsConjRoot K L.

LaTeX

$$$\mathrm{ConjRootClass}(K,L) = L / \sim_{\!K,L}$, где $\sim$ — отношение IsConjRoot K L$$

Lean4

/-- `ConjRootClass K L` is the quotient of `L` by the relation `IsConjRoot K`. -/
def ConjRootClass :=
  Quotient (α := L) (IsConjRoot.setoid K L)

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

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

Разделы

Аффилиация

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