Commit 2024-10-19 22:21 e0dccaab

View on Github →

chore(FieldTheory/Galois): Move infinite Galois (#17945) Split the original file FieldTheory.Galois.Infinite into GaloisClosure and Profinite, for spliting the basic constructions, profinite (stated categorically), and the fundamental theorem completely. Moves:

Mathlib.FieldTheory.Galois.Infinite -> Mathlib.FieldTheory.Galois.GaloisClosure
Mathlib.FieldTheory.Galois.Infinite -> Mathlib.FieldTheory.Galois.Profinite

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/FieldTheory/Galois/Infinite.lean to Mathlib/FieldTheory/Galois/GaloisClosure.lean

deleted def FiniteGaloisIntermediateField.finGaloisGroup

deleted theorem finGaloisGroupMap.map_comp

deleted theorem finGaloisGroupMap.map_id

Created Mathlib/FieldTheory/Galois/Profinite.lean

added def FiniteGaloisIntermediateField.finGaloisGroup

added theorem finGaloisGroupMap.map_comp

added theorem finGaloisGroupMap.map_id