root

Mathlib.RingTheory.IsAdjoinRoot

URI: https://scilib.ai/kg/mathlib#IsAdjoinRoot.root

English

For an IsAdjoinRoot S f, the image of the indeterminate X under the structure map equals the root of f in S.

Русский

Для IsAdjoinRoot S f образ индетерминированной переменной X под действием структуры равен корню f в S.

LaTeX

$$$h.map X = h.root$$$

Lean4

/-- `(h : IsAdjoinRoot S f).root` is the root of `f` that can be adjoined to generate `S`. -/
def root : S :=
  h.map X

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

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

Разделы

Аффилиация

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