separableClosure_eq_bot — Mathlib

English

The separable closure inside its own separable closure is equal to the bottom field.

Русский

Разделимое замыкание внутри самого себя равно нулю/нижнему полю.

LaTeX

$$separableClosure (separableClosure F E) E = ⊥$$

Lean4

/-- The separable closure in `E` of the separable closure of `F` in `E` is equal to itself. -/
theorem separableClosure_eq_bot : separableClosure (separableClosure F E) E = ⊥ :=
  bot_unique fun x hx ↦
    mem_bot.2 ⟨⟨x, IsSeparable.of_algebra_isSeparable_of_isSeparable F (mem_separableClosure_iff.1 hx)⟩, rfl⟩

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