Commit 2024-09-11 04:47 d46e3640

View on Github →

feat(FieldTheory/{SeparableDegree|PurelyInseparable}): generalize some results on purely inseparable extension to non-commutative case (#16585)

generalize the result on separable degree of minpoly to non-commutative case
generalize the definition and basic property of purely inseparable extension to non-commutative case This PR is potentially usable in #16525.

Estimated changes

Modified Mathlib/FieldTheory/PurelyInseparable.lean

modified theorem Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed

modified theorem IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable

modified theorem IsPurelyInseparable.isAlgebraic

modified theorem IsPurelyInseparable.pow_mem

added theorem Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable

modified theorem isPurelyInseparable_iff_pow_mem

modified theorem separableClosure.eq_bot_iff

modified theorem separableClosure.eq_bot_of_isPurelyInseparable

Modified Mathlib/FieldTheory/SeparableDegree.lean