isSeparable — Mathlib

English

The separable closure is separable over F.

Русский

Разделимое замыкание над F является разделимым над F.

LaTeX

$$$\\operatorname{IsSeparable} F (\\text{separableClosure } F E)$$$

Lean4

/-- The separable closure of `F` in `E` is separable over `F`. -/
@[stacks 030K "$E_{sep}/F$ is separable"]
instance isSeparable : Algebra.IsSeparable F (separableClosure F E) :=
  ⟨fun x ↦ by simpa only [IsSeparable, minpoly_eq] using x.2⟩

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