Theorem Subgroup.MapSubtype.orderIso_symm_apply

Modification history

2025-06-08 14:09
Mathlib/Algebra/Group/Subgroup/Ker.lean
feat: `Subgroup ↥(H : Subgroup G) ≃o { H' : Subgroup G // H' ≤ H }` (#25367) …
Added Subgroup.MapSubtype.orderIso_symm_applyView on Github →