Theorems · Inductive type · group theory
AddRightCancelSemigroup
Type u → Type u
An AddRightCancelSemigroup is an additive semigroup such that
a + b = c + b implies a = c.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 41 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
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 by63
Results whose statement or proof uses this declaration.
- CochainComplexstatement and proof · cited by 1,016
- ChainComplexstatement and proof · cited by 350
- ChainComplex.of.dstatement and proof · cited by 16
- CochainComplex.of.dstatement and proof · cited by 15
- CochainComplex.nextstatement and proof · cited by 13
- CategoryTheory.Idempotents.karoubiChainComplexEquivalencestatement and proof · cited by 13
- CategoryTheory.Idempotents.karoubiCochainComplexEquivalencestatement and proof · cited by 12
- ChainComplex.of_dstatement and proof · cited by 9
- ChainComplex.linearYonedaObjstatement and proof · cited by 6
- ChainComplex.prevstatement and proof · cited by 6
- CochainComplex.of_dstatement and proof · cited by 4
- ChainComplex.ofstatement and proof · cited by 4