Theorems · Definition · group theory
AddSubmonoid.toSubmonoid
{A : Type u_4} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)Additive submonoids of an additive monoid A are isomorphic to
multiplicative submonoids of Multiplicative A.
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- AddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- SetLike.coeproof · cited by 8,199
- Set.preimageproof · cited by 4,946
- Submonoidstatement and proof · cited by 3,086
- AddZeroClassstatement and proof · cited by 1,237
- AddSubmonoidstatement and proof · cited by 1,178
- Multiplicativestatement and proof · cited by 875
- OrderIsostatement · cited by 874
- Multiplicative.ofAddproof · cited by 237
- Multiplicative.toAddproof · cited by 161
- AddSubmonoid.zero_mem'proof · cited by 1
Cited by7
Results whose statement or proof uses this declaration.
- Subgroup.toAddSubgroupproof · cited by 20
- AddSubgroup.toSubgroupproof · cited by 15
- AddSubmonoid.fg_iff_mul_fgstatement and proof · cited by 2
- Submonoid.toAddSubmonoid'proof · cited by 1
- AddSubmonoid.coe_toSubmonoid_symm_applystatement and proof · cited by 0
- AddSubmonoid.coe_toSubmonoid_applystatement and proof · cited by 0
- AddSubmonoid.toSubmonoid_closurestatement and proof · cited by 0