isSeparable

Mathlib.FieldTheory.IsSepClosed

URI: https://scilib.ai/kg/mathlib#IsSepClosure.isSeparable

English

If k ⊂ K with IsSepClosure k K, then Algebra.IsSeparable k K holds.

Русский

Если есть IsSepClosure k K, то существует Algebra.IsSeparable k K.

LaTeX

$$Algebra.IsSeparable k K$$

Lean4

instance isSeparable [Algebra k K] [IsSepClosure k K] : Algebra.IsSeparable k K :=
  IsSepClosure.separable

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

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

Разделы

Аффилиация

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