perfectField_iff_isSeparable_algebraicClosure

English

Under separability, mapping a basis via q-power operations yields another valid basis sequence.

Русский

При разделяемости отображение базиса через q-возведение образует другую корректную перестановку базиса.

LaTeX

$$$\text{new basis} = \{ b_i^{q^n} \}$ is a basis$$

Lean4

/-- If `E` is an algebraic closure of `F`, then `F` is perfect if and only if `E / F` is
separable. -/
theorem perfectField_iff_isSeparable_algebraicClosure [IsAlgClosure F E] : PerfectField F ↔ Algebra.IsSeparable F E :=
  ⟨fun _ ↦ IsSepClosure.separable, fun _ ↦
    haveI : IsAlgClosed E := IsAlgClosure.isAlgClosed F
    perfectField_of_isSeparable_of_perfectField_top F E⟩

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