instNeZeroSepDegree

Mathlib.FieldTheory.SeparableClosure

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

English

The separable degree is nonzero: sepDegree F E ≠ 0.

Русский

Сепарабельная степень не равна нулю: sepDegree F E ≠ 0.

LaTeX

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

Lean4

instance instNeZeroSepDegree : NeZero (sepDegree F E) :=
  ⟨rank_pos.ne'⟩

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

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

Разделы

Аффилиация

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