Commit 2025-07-30 17:21 1f310e43

View on Github →

refactor(FieldTheory/Galois): Switch from Fintype to Finite (#25997) This PR switches mathlib's Galois theory from Fintype to Finite to match the group theory library.

Estimated changes

Modified Mathlib/FieldTheory/Galois/Basic.lean

modified theorem IntermediateField.finrank_fixedField_eq_card

modified theorem IsGalois.card_fixingSubgroup_eq_finrank

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/FieldTheory/KrullTopology.lean

Modified Mathlib/FieldTheory/KummerExtension.lean

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

modified theorem Polynomial.Gal.card_of_separable

Modified Mathlib/NumberTheory/NumberField/CMField.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

modified theorem IsUnramifiedAtInfinitePlaces_of_odd_card_aut

modified theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified

modified theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn