Commit 2026-06-20 15:40 0bee4471

View on Github →

refactor(FieldTheory/Galois/IsGaloisGroup): generalize mulEquivAlgEquiv to domains (#40822) This PR generalizes mulEquivAlgEquiv to domains. This allows us to remove mulEquivCongr' (a field version of mulEquivCongr).

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

modified theorem IsGaloisGroup.card_eq_finrank'

modified theorem IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup

deleted theorem IsGaloisGroup.mulEquivCongr'_apply_smul

modified theorem IsGaloisGroup.mulEquivCongr_apply_smul

modified theorem IsGaloisGroup.mulEquivCongr_symm_apply_smul

Modified Mathlib/Logic/Function/Basic.lean

added theorem Function.Bijective.of_comp_left