Commit 2023-08-01 16:05 bee2977f

View on Github →

refactor(FieldTheory/NormalClosure): move to new file (#6273) This PR moves normalClosure to a separate file, in preparation for #6163.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Galois.lean

Modified Mathlib/FieldTheory/Normal.lean

deleted theorem normalClosure.restrictScalars_eq_iSup_adjoin

Created Mathlib/FieldTheory/NormalClosure.lean

added theorem normalClosure.restrictScalars_eq_iSup_adjoin