Theorems · Definition · group theory
AddSubgroup.topEquiv
{G : Type u_1} → [inst : AddGroup G] → ↥⊤ ≃+ GThe top additive subgroup is isomorphic to the additive group.
This is the additive group version of AddSubmonoid.topEquiv.
- Defined in
- Mathlib.Algebra.Group.Subgroup.Lattice
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext
- Assumes
- AddGroup
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
- AddGroupstatement and proof · cited by 4,410
- AddSubgroupstatement · cited by 3,232
- AddEquivstatement · cited by 1,087
- AddSubmonoid.topEquivproof · cited by 4
Cited by10
Results whose statement or proof uses this declaration.
- AddSubgroup.card_topproof · cited by 3
- AddGroup.isNilpotent_topproof · cited by 2
- AddGroup.isAddCyclic_of_coprime_card_range_card_kerproof · cited by 1
- AddAction.isBlock_topproof · cited by 1
- AddGroup.fintypeOfKerOfCodomproof · cited by 0
- AddSubgroup.topEquiv_applystatement and proof · cited by 0
- AddSubgroup.topEquiv_symm_apply_coestatement and proof · cited by 0
- AddGroup.isAddCyclic_prod_iffproof · cited by 0
- AddSubgroup.exponent_topproof · cited by 0
- AddSubgroup.ofAddUnitsTopEquivproof · cited by 0