of_integral

Mathlib.FieldTheory.Separable

URI: https://scilib.ai/kg/mathlib#IsSeparable.of_integral

English

An integral field extension in characteristic 0 is separable.

Русский

Целочисленное расширение поля в характеристике 0 разделяемо.

LaTeX

$$protected instance (priority := 100) of_integral : Algebra.IsSeparable F K := ⟨_root_.IsSeparable.of_integral _⟩$$

Lean4

theorem of_integral (x : K) : IsSeparable F x :=
  (minpoly.irreducible <| Algebra.IsIntegral.isIntegral x).separable

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

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

Разделы

Аффилиация

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