Theorem IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable
Modification history
2025-02-03 08:48
Mathlib/FieldTheory/PurelyInseparable.lean
refactor(FieldTheory): split `Mathlib.FieldTheory.Purelyinseparable` (#21343)
Modified IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparableView on Github →