Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-15 02:43 591ff3a5

View on Github →

feat(group_theory/subgroup): Subgroup of subgroup is isomorphic to itself (#9204) If H ≤ K, then H as a subgroup of K is isomorphic to H.

Estimated changes