Theorems · Inductive type · group theory
IsLeftCancelVAdd
(G : Type u_9) → (P : Type u_10) → [VAdd G P] → Prop
A vector addition is left-cancellative if it is pointwise injective on the left.
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- VAdd
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.
- VAddstatement · cited by 616
Cited by12
Results whose statement or proof uses this declaration.
- Set.VAddAntidiagonal.finite_of_finitestatement and proof · cited by 5
- AddMonoidAlgebra.smul_eqstatement and proof · cited by 2
- IsLeftCancelVAdd.left_cancelstatement and proof · cited by 2
- IsLeftCancelVAdd.left_cancel'statement and proof · cited by 2
- Set.VAddAntidiagonal.eq_of_fst_eq_fststatement and proof · cited by 1
- Finset.pairwiseDisjoint_vadd_iffstatement and proof · cited by 1
- Set.pairwiseDisjoint_vadd_iffstatement and proof · cited by 1
- IsLeftCancelVAdd.recOnstatement and proof · cited by 0
- IsCancelVAdd.casesOnstatement and proof · cited by 0
- IsCancelVAdd.recOnstatement and proof · cited by 0
- Finsupp.smul_eqstatement · cited by 0
- IsLeftCancelVAdd.casesOnstatement and proof · cited by 0