Theorems · Inductive type · group theory
AddSubsemigroup
(M : Type u_3) → [Add M] → Type u_3
An additive subsemigroup of an additive magma M is a subset closed under addition.
- Defined in
- Mathlib.Algebra.Group.Subsemigroup.Defs
- Cited by
- 262 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- Add
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by318
Results whose statement or proof uses this declaration.
- AddSubmonoid.toAddSubsemigroupstatement · cited by 198
- AddSubsemigroup.carrierstatement and proof · cited by 198
- AddSubsemigroup.mapstatement and proof · cited by 50
- AddSubsemigroup.comapstatement and proof · cited by 39
- AddSubsemigroup.closurestatement and proof · cited by 34
- AddSubsemigroup.opstatement and proof · cited by 28
- AddSubsemigroup.unopstatement and proof · cited by 25
- AddSubsemigroup.centerstatement · cited by 19
- AddSubsemigroup.opEquivstatement and proof · cited by 18
- AddHom.srangestatement · cited by 17
- AddSubsemigroup.gc_map_comapstatement and proof · cited by 15
- AddSubmonoid.mk.congr_simpstatement and proof · cited by 14
Showing the 200 most cited of 318.