Commit 2024-03-01 09:34 f56665db

View on Github →

feat(FieldTheory/PurelyInseparable): some more results for purely inseparable extension (#10882)

  • perfectClosure.perfect(Ring|Field): if E is a perfect field of characteristic p, then the (relative) perfect closure perfectClosure F E is perfect.
  • Is[PurelyIn]separable.[fin][In]sepDegree_eq: various degrees of a [purely in]separable extension
  • IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable[']: if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any subset S of K such that F(S) / F is algebraic, the E(S) / E and F(S) / F have the same separable degree.
  • minpoly.map_eq_of_separable_of_isPurelyInseparable: if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any element x of K separable over F, it has the same minimal polynomials over F and over E.
  • Polynomial.Separable.map_irreducible_of_isPurelyInseparable: if E / F is a purely inseparable field extension, f is a separable irreducible polynomial over F, then it is also irreducible over E.

Estimated changes