adjoinRootAlgEquiv_apply_root

Mathlib.RingTheory.IsAdjoinRoot

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

English

Applying the root element to AdjoinRoot yields the root element mapped by h.

Русский

Замена корня в AdjoinRoot приводит к корню через h.

LaTeX

$$$h.adjoinRootAlgEquiv(\operatorname{AdjoinRoot.root} f) = h.root$$$

Lean4

@[simp]
theorem adjoinRootAlgEquiv_apply_root : h.adjoinRootAlgEquiv (AdjoinRoot.root f) = h.root :=
  rfl

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

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

Разделы

Аффилиация

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