Commit 2023-12-07 22:15 e09fd6dd

View on Github →

feat(FieldTheory/Separable): add AlgEquiv.isSeparable, AlgEquiv.isSeparable_iff and IsSeparable.isAlgebraic (#8861)

  • add AlgEquiv.isSeparable, AlgEquiv.isSeparable_iff which states that IsSeparable is invariant under AlgEquiv
  • also add IsSeparable.isAlgebraic which states that separable extension is algebraic

Estimated changes

added theorem AlgEquiv.isSeparable