instNeZeroInsepDegree

Mathlib.FieldTheory.SeparableClosure

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

English

In the finite-dimensional case, insepDegree F E is nonzero.

Русский

В случае конечной размерности insepDegree F E не ноль.

LaTeX

$$$\\mathrm{NeZero}(\\mathrm{insepDegree}(F,E))$$$

Lean4

instance instNeZeroInsepDegree : NeZero (insepDegree F E) :=
  ⟨rank_pos.ne'⟩

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

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

Разделы

Аффилиация

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