separable

Mathlib.FieldTheory.Galois.Basic

URI: https://scilib.ai/kg/mathlib#IsGalois.separable

English

For any x ∈ E, if E/F is IsGalois, then x is separable over F.

Русский

Для любого x ∈ E, если E/F Галуа, то x есть раздельно над F.

LaTeX

$$$\\text{IsGalois } F E \\Rightarrow \\forall x, \\ IsSeparable F x$$$

Lean4

theorem separable [IsGalois F E] (x : E) : IsSeparable F x :=
  Algebra.IsSeparable.isSeparable F x

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

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

Разделы

Аффилиация

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