Theorems · Definition · group theory
Subgroup.topEquiv
{G : Type u_1} → [inst : Group G] → ↥⊤ ≃* GThe top subgroup is isomorphic to the group.
This is the group version of Submonoid.topEquiv.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Lattice
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- Group
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement · cited by 9,680
- Groupstatement and proof · cited by 6,238
- Subgroupstatement · cited by 3,593
- MulEquivstatement · cited by 1,142
- Submonoid.topEquivproof · cited by 4
Cited by13
Results whose statement or proof uses this declaration.
- Subgroup.card_topproof · cited by 3
- Group.isCyclic_prod_iffproof · cited by 2
- ClassGroup.equivPicproof · cited by 2
- Group.isCyclic_of_coprime_card_range_card_kerproof · cited by 1
- Group.isNilpotent_topproof · cited by 1
- MulAction.isBlock_topproof · cited by 1
- Subgroup.ofUnitsTopEquivproof · cited by 0
- Subgroup.exponent_topproof · cited by 0
- Group.fintypeOfKerOfCodomproof · cited by 0
- IsGaloisGroup.top_iffproof · cited by 0
- Subgroup.topEquiv_applystatement and proof · cited by 0
- Subgroup.topEquiv_symm_apply_coestatement and proof · cited by 0