Commit 2026-06-18 19:42 113f7cc9
View on Github →refactor(FieldTheory/*): swap imports of IsSepClosed and SeparableClosure (#40777)
This PR swaps the imports order between IsSepClosed.lean and SeparableClosure.lean. This allows basic facts like adjoining separable elements gives a separable extension to be used to golf a proof in Galois/Basic.lean.
These basic facts basically require knowing the existence of the separable closure, but right now SeparableClosure.lean imports IsSepClosed.lean which imports Galois/Basic.lean.
This PR is a slight modification of #40339.