Theorem IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup

Modification history

2026-06-20 15:40

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

refactor(FieldTheory/Galois/IsGaloisGroup): generalize `mulEquivAlgEquiv` to domains (#40822) …

Modified IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup View on Github →

2025-11-27 08:19

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

feat(FieldTheory/IsGaloisGroup): prove the Galois correspondence for `IsGaloisGroup` (#29688) …

Added IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup View on Github →