finInsepDegree_self

Mathlib.FieldTheory.SeparableClosure

URI: https://scilib.ai/kg/mathlib#Field.finInsepDegree_self

English

For any field F, the finite inseparable degree of the identity extension F/F is 1.

Русский

Для произвольного поля F конечная неинsep-степень расширения F/F равна 1.

LaTeX

$$$ \mathrm{finInsepDegree}(F,F) = 1$$$

Lean4

@[simp]
theorem finInsepDegree_self : finInsepDegree F F = 1 := by
  rw [finInsepDegree_def', insepDegree_self, Cardinal.one_toNat]

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

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

Разделы

Аффилиация

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