instNeZeroFinInsepDegree

Mathlib.FieldTheory.SeparableClosure

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

English

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

Русский

В конечном размерном случае finInsepDegree F E не ноль.

LaTeX

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

Lean4

instance instNeZeroFinInsepDegree [FiniteDimensional F E] : NeZero (finInsepDegree F E) :=
  ⟨finrank_pos.ne'⟩

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

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

Разделы

Аффилиация

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