mem_separableClosure_iff — Mathlib

English

An element lies in the separable closure iff it is separable over the base field.

Русский

Элемент лежит в разделимом замыкании тогда и только тогда, когда он разделим над осн. полем.

LaTeX

$$$x \\in separableClosure F E \\;\\Leftrightarrow\\; IsSeparable F x$$$

Lean4

/-- An element is contained in the separable closure of `F` in `E` if and only if
it is a separable element. -/
theorem mem_separableClosure_iff {x : E} : x ∈ separableClosure F E ↔ IsSeparable F x :=
  Iff.rfl

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