Commit 2026-05-28 16:06 29c689a8

View on Github →

chore(IsGaloisGroup): refactor IsGaloisGroup.quotient (#38153) Refactors the quotient construction in IsGaloisGroup to work at the level of ring extensions rather than intermediate fields.

Estimated changes

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

added theorem IsGaloisGroup.algebraMap_smulOfNormal

deleted theorem IsGaloisGroup.coe_quotient_smul

added theorem IsGaloisGroup.isScalarTower_mulSemiringActionQuotient

added theorem IsGaloisGroup.map_quotientMk'

added theorem IsGaloisGroup.mulSemiringActionQuotient_smul_def

added theorem IsGaloisGroup.quotient

deleted theorem IsGaloisGroup.quotientMap

added def IsGaloisGroup.smulCommClassQuotient

deleted theorem IsGaloisGroup.smul_eq_self

modified theorem IsGaloisGroup.smul_mem_of_normal

Modified Mathlib/GroupTheory/GroupAction/Quotient.lean

added theorem MulAction.coe_quotient_smul