isSeparable_self

Mathlib.FieldTheory.Separable

URI: https://scilib.ai/kg/mathlib#Algebra.isSeparable_self

English

The field F is isomorphic to itself, hence separable over itself.

Русский

Поле F само по себе, следовательно separable над собой.

LaTeX

$$instance isSeparable_self : Algebra.IsSeparable F F := ⟨isSeparable_algebraMap⟩$$

Lean4

instance isSeparable_self : Algebra.IsSeparable F F :=
  ⟨isSeparable_algebraMap⟩

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

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

Разделы

Аффилиация

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