Commit 2026-02-16 09:35 43d5379b

View on Github →

feat(IsGaloisGroup): add IsGaloisGroup.of_mulEquiv (#35310) This PR adds the IsGaloisGroup.of_mulEquiv lemma stating that IsGaloisGroup is preserved under group isomorphisms.

Estimated changes