isSeparable_of_mem_isSeparable — Mathlib

English

If L is an intermediate field of E/F that is separable over F, then any x ∈ L is separable over F.

Русский

Если L ⊆ E является внутренним полем над F и L сепарабельно над F, то любой элемент x ∈ L сепарабелен над F.

LaTeX

$$$ x \in L \Rightarrow IsSeparable F x $$$

Lean4

theorem isSeparable_of_mem_isSeparable {L : IntermediateField F E} [Algebra.IsSeparable F L] {x : E} (h : x ∈ L) :
    IsSeparable F x := by simpa only [IsSeparable, minpoly_eq] using Algebra.IsSeparable.isSeparable F (K := L) ⟨x, h⟩

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