Theorem IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDual

Modification history

2025-11-27 08:19
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
feat(FieldTheory/IsGaloisGroup): prove the Galois correspondence for `IsGaloisGroup` (#29688) …
Added IsGaloisGroup.intermediateFieldEquivSubgroup_symm_apply_toDualView on Github →