Commit 2025-06-08 14:09 9dbb163e
View on Github →feat: Subgroup ↥(H : Subgroup G) ≃o { H' : Subgroup G // H' ≤ H } (#25367)
This is required to prove that A_n is simple iff n = 3 or 5 ≤ n: #23555
feat: Subgroup ↥(H : Subgroup G) ≃o { H' : Subgroup G // H' ≤ H } (#25367)
This is required to prove that A_n is simple iff n = 3 or 5 ≤ n: #23555