Commit 2026-05-29 18:27 a66e8da4

View on Github →

feat(FieldTheory/Galois/IsGaloisGroup): generalize mulEquivCongr (#38464) Generalizes mulEquivCongr from field extensions to domain extensions. The field version is renamed to mulEquivCongr'. Also adds some simp lemmas.

Estimated changes

Modified Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

modified theorem IsGaloisGroup.fixingSubgroup_range_algebraMap

added theorem IsGaloisGroup.mulEquivCongr'_apply_smul

modified theorem IsGaloisGroup.mulEquivCongr_apply_smul

added theorem IsGaloisGroup.mulEquivCongr_symm_apply_smul