Theorems · Definition · group theory
Submonoid.toAddSubmonoid
{M : Type u_1} → [inst : MulOneClass M] → Submonoid M ≃o AddSubmonoid (Additive M)Submonoids of monoid M are isomorphic to additive submonoids of Additive M.
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 25 from the axioms · uses propext, Quot.sound
- Assumes
- MulOneClass
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
- AddSubmonoidstatement and proof · cited by 1,178
- MulOneClassstatement and proof · cited by 1,018
- OrderIsostatement · cited by 874
- Additivestatement and proof · cited by 356
- Additive.ofMulproof · cited by 155
- Additive.toMulproof · cited by 109
- Submonoid.one_mem'proof · cited by 3
Cited by8
Results whose statement or proof uses this declaration.
- Subgroup.toAddSubgroupproof · cited by 20
- AddSubgroup.toSubgroupproof · cited by 15
- Submonoid.fg_iff_add_fgstatement and proof · cited by 3
- AddSubmonoid.fg_iff_mul_fgproof · cited by 2
- AddSubmonoid.toSubmonoid'proof · cited by 2
- Submonoid.toAddSubmonoid_closurestatement and proof · cited by 0
- Submonoid.coe_toAddSubmonoid_applystatement and proof · cited by 0
- Submonoid.coe_toAddSubmonoid_symm_applystatement and proof · cited by 0