Commit 2026-06-23 14:13 d5c56094

View on Github →

chore(FieldTheory/IsGaloisGroup): split file by imports (#40942) This PR splits off the ring-theoretic part of FieldTheory/IsGaloisGroup.lean to the RingTheory folder.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

deleted theorem IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply

deleted theorem IsGaloisGroup.algebraMap_ringEquiv_apply

deleted theorem IsGaloisGroup.algebraMap_ringEquiv_symm_apply

deleted theorem IsGaloisGroup.algebraMap_smulOfNormal

deleted theorem IsGaloisGroup.iff_isFractionRing

deleted theorem IsGaloisGroup.iff_of_mulEquiv

deleted theorem IsGaloisGroup.mulSemiringActionQuotient_smul_def

deleted theorem IsGaloisGroup.of_algEquiv

deleted theorem IsGaloisGroup.of_isFractionRing

deleted theorem IsGaloisGroup.of_mulEquiv

deleted theorem IsGaloisGroup.of_ringEquiv

deleted theorem IsGaloisGroup.of_ringHom_surjective

deleted def IsGaloisGroup.smulCommClassQuotient

deleted theorem IsGaloisGroup.smul_mem_of_normal

deleted theorem IsGaloisGroup.to_isFractionRing

deleted theorem IsGaloisGroup.to_isFractionRing_of_isIntegral

deleted theorem IsGaloisGroup.top_iff

Created Mathlib/RingTheory/IsGaloisGroup/Basic.lean

added theorem IsGaloisGroup.algebraMap_smulOfNormal

added theorem IsGaloisGroup.iff_isFractionRing

added theorem IsGaloisGroup.mulSemiringActionQuotient_smul_def

added theorem IsGaloisGroup.of_isFractionRing

added def IsGaloisGroup.smulCommClassQuotient

added theorem IsGaloisGroup.smul_mem_of_normal

added theorem IsGaloisGroup.to_isFractionRing

added theorem IsGaloisGroup.to_isFractionRing_of_isIntegral

Created Mathlib/RingTheory/IsGaloisGroup/Defs.lean

added theorem IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply

added theorem IsGaloisGroup.algebraMap_ringEquiv_apply

added theorem IsGaloisGroup.algebraMap_ringEquiv_symm_apply

added theorem IsGaloisGroup.iff_of_mulEquiv

added theorem IsGaloisGroup.of_algEquiv

added theorem IsGaloisGroup.of_mulEquiv

added theorem IsGaloisGroup.of_ringEquiv

added theorem IsGaloisGroup.of_ringHom_surjective

added theorem IsGaloisGroup.top_iff