Theorems · Inductive type · group theory
IsCancelAdd
(G : Type u) → [Add G] → Prop
A mixin for cancellative addition.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 79 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 by86
Results whose statement or proof uses this declaration.
- AddMonoidAlgebra.divOfstatement and proof · cited by 17
- AddMonoidAlgebra.coeff_single_mul_addstatement and proof · cited by 3
- Matrix.isLeftRegular_iff_nonsingularstatement and proof · cited by 3
- AddMonoidAlgebra.divOf_add_modOfstatement and proof · cited by 3
- Matrix.Nonsingular.linearIndependent_colstatement and proof · cited by 2
- Set.AddAntidiagonal.fst_eq_fst_iff_snd_eq_sndstatement and proof · cited by 2
- Matrix.linearIndependent_col_iffstatement and proof · cited by 2
- Matrix.linearIndependent_row_iffstatement and proof · cited by 2
- addLeftEmbedding_eq_addRightEmbeddingstatement and proof · cited by 2
- AddMonoidAlgebra.mul_of'_divOfstatement and proof · cited by 2
- Function.Injective.isCancelAddstatement and proof · cited by 2
- AddMonoidAlgebra.coeff_divOfstatement and proof · cited by 2