Theorems · Inductive type · group theory
AddSubmonoid
(M : Type u_3) → [AddZeroClass M] → Type u_3
An additive submonoid of an additive monoid M is a subset containing 0 and
closed under addition.
- Defined in
- Mathlib.Algebra.Group.Submonoid.Defs
- Cited by
- 1,178 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
- Assumes
- AddZeroClass
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddZeroClassstatement · cited by 1,237
Cited by1,465
Results whose statement or proof uses this declaration.
- Submodule.mapproof · cited by 614
- Submodule.comapproof · cited by 347
- IsLocalRing.maximalIdealproof · cited by 297
- AddSubmonoid.closurestatement and proof · cited by 224
- AddSubmonoid.toAddSubsemigroupstatement and proof · cited by 198
- AddSubgroup.mapproof · cited by 189
- Submodule.toAddSubmonoidstatement · cited by 162
- AddMonoidHom.kerproof · cited by 158
- AddSubgroup.comapproof · cited by 123
- AddSubmonoid.LocalizationMapstatement · cited by 119
- AddAction.stabilizerproof · cited by 112
- Submodule.toAddSubgroupproof · cited by 106
Showing the 200 most cited of 1,465.