mk_def

Mathlib.FieldTheory.Minpoly.ConjRootClass

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

English

The quotient class of x equals the canonical mk K x.

Русский

Класс эквивалентности элемента x равен каноническому mk K x.

LaTeX

$$$\lVert x \rVert = \mathrm{mk}_K(x)$$$

Lean4

@[simp]
theorem mk_def {x : L} : ⟦x⟧ = mk K x :=
  rfl

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

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

Разделы

Аффилиация

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