isSeparable_inv — Mathlib

English

For α algebraic over F, finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ iff IsSeparable F α (alternative formulation).

Русский

Для α над F алгебраичен, тогда finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ тогда и только тогда IsSeparable F α (альтернативная формулировка).

LaTeX

$$$ finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ \iff IsSeparable F α $$$

Lean4

/-- If `x` is a separable element, then `x⁻¹` is also a separable element. -/
theorem isSeparable_inv {x : E} (hx : IsSeparable F x) : IsSeparable F x⁻¹ :=
  haveI := (isSeparable_adjoin_simple_iff_isSeparable F E).2 hx
  isSeparable_of_mem_isSeparable F E <| F⟮x⟯.inv_mem <| mem_adjoin_simple_self F x

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