Commit 2024-01-08 14:36 417f344b

View on Github →

feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field (#9522)

  • IsSepClosure.isAlgClosure_of_perfectField, IsSepClosure.of_isAlgClosure_of_perfectField: if k is a perfect field, then its separable closure coincides with its algebraic closure.
  • IsSepClosed.isAlgClosed_of_perfectField: a separably closed perfect field is also algebraically closed.
  • Algebra.IsAlgebraic.[isSeparable_of_]perfectField: if L / K is an algebraic extension, K is a perfect field, then L / K is separable and L is perfect.

Estimated changes