Theorem IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply

Modification history

2026-06-23 14:13
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
chore(FieldTheory/IsGaloisGroup): split file by imports (#40942) …
Modified IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_applyView on Github →
2026-03-04 18:26
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
feat(IsGaloisGroup): if `B/A` and `B/A'` are Galois with the same Galois group, then `A ≃+* A'` (#35797)
Added IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_applyView on Github →