botEquiv_def

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

URI: https://scilib.ai/kg/mathlib#IntermediateField.botEquiv_def

English

The evaluation of the bottom equivalence on a base element x yields x.

Русский

Проверка действия нижней эквивалентности на элементе базового поля даёт тот же элемент.

LaTeX

$$$ botEquiv(F,E)(algebraMap(F,(\\bot : \\text{IntermediateField}(F,E))\,x)) = x $$$

Lean4

theorem botEquiv_def (x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x := by simp

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

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

Разделы

Аффилиация

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