Commit 2025-02-03 08:48 347a323d

View on Github →

refactor(FieldTheory): split Mathlib.FieldTheory.Purelyinseparable (#21343)

Estimated changes

deleted theorem Field.finSepDegree_eq
deleted theorem IsPurelyInseparable.trans
deleted theorem eq_separableClosure
deleted theorem eq_separableClosure_iff
deleted theorem isPurelyInseparable_iff
deleted theorem le_perfectClosure
deleted theorem le_perfectClosure_iff
deleted theorem mem_perfectClosure_iff
deleted def perfectClosure
deleted theorem separableClosure_le
deleted theorem separableClosure_le_iff
added theorem Field.finSepDegree_eq
added theorem eq_separableClosure
added theorem separableClosure_le
added theorem le_perfectClosure
added theorem le_perfectClosure_iff
added theorem mem_perfectClosure_iff
added def perfectClosure