Commit 2024-09-19 08:44 9ba85757

View on Github →

feat(FieldTheory/Separable): Add lemmas of elementwise IsSeparable (#14404) Add lemmas of elementwise IsSeparable decomposed from Algebra.IsSeparable lemmas. Add Field.isSeparable_neg, Field.isSeparable_sub

Estimated changes

Modified Mathlib/FieldTheory/PurelyInseparable.lean

Modified Mathlib/FieldTheory/Separable.lean

added theorem AlgEquiv.Algebra.isSeparable

added theorem AlgEquiv.Algebra.isSeparable_iff

deleted theorem AlgEquiv.isSeparable

modified theorem AlgEquiv.isSeparable_iff

modified theorem Algebra.IsSeparable.of_algHom

modified theorem Algebra.IsSeparable.of_equiv_equiv

added theorem IsSeparable.of_algHom

added theorem IsSeparable.of_equiv_equiv

added theorem IsSeparable.of_integral

deleted theorem IsSeparable.of_isScalarTower

added theorem IsSeparable.tower_bot

added theorem IsSeparable.tower_top

added theorem isSeparable_algebraMap

Modified Mathlib/FieldTheory/SeparableClosure.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

added theorem Field.isSeparable_neg

added theorem Field.isSeparable_sub