botEquiv_symm

Mathlib.FieldTheory.IntermediateField.Adjoin.Defs

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

English

The inverse of the bottom equivalence sends a base element x to the canonical algebra map image of x.

Русский

Обратное к нижней эквивалентности отображает элемент x в образ алгебраического отображения x.

LaTeX

$$$ (botEquiv F E)^{-1}(x) = algebraMap F E (x) $$$

Lean4

@[simp]
theorem botEquiv_symm (x : F) : (botEquiv F E).symm x = algebraMap F _ x :=
  rfl

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

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

Разделы

Аффилиация

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