eq_bot_of_isSeparable — Mathlib

English

If E/F is separable, then the perfect closure equals the bottom field ⊥.

Русский

Если E/F разделимо, то совершенное замыкание равно нижнему полю ⊥.

LaTeX

$$[Algebra.IsSeparable F E] ⇒ perfectClosure F E = ⊥$$

Lean4

/-- If `E / F` is separable, then the perfect closure of `F` in `E` is equal to `F`. Note that
  the converse is not necessarily true (see https://math.stackexchange.com/a/3009197)
  even when `E / F` is algebraic. -/
theorem eq_bot_of_isSeparable [Algebra.IsSeparable F E] : perfectClosure F E = ⊥ :=
  haveI := Algebra.isSeparable_tower_bot_of_isSeparable F (perfectClosure F E) E
  eq_bot_of_isPurelyInseparable_of_isSeparable _

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