Theorems · Inductive type · group theory
IsLeftCancelAdd
(G : Type u) → [Add G] → Prop
A mixin for left cancellative addition.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 1 from the axioms · 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 by94
Results whose statement or proof uses this declaration.
- add_right_injstatement and proof · cited by 71
- add_eq_leftstatement and proof · cited by 37
- addLeftEmbeddingstatement and proof · cited by 36
- add_right_injectivestatement and proof · cited by 36
- add_left_cancelstatement and proof · cited by 29
- add_left_cancel_iffstatement and proof · cited by 17
- left_eq_addstatement and proof · cited by 15
- addLeftEmbedding_applystatement and proof · cited by 9
- IsAddLeftRegular.allstatement and proof · cited by 5
- Finset.card_le_card_add_leftstatement and proof · cited by 4
- Finset.card_singleton_addstatement and proof · cited by 3
- Function.Injective.isLeftCancelAddstatement and proof · cited by 3