Theorems · Theorem · group theory
zero_vadd
∀ (M : Type u_1) {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α] (b : α), 0 +ᵥ b = b- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 95 results in Mathlib
- Foundations
- Depth 7 from the axioms, rests on 33 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddMonoidstatement and proof · cited by 2,864
- HVAdd.hVAddstatement · cited by 1,820
- AddActionstatement and proof · cited by 820
- AddAction.zero_vaddproof · cited by 1
Cited by96
Results whose statement or proof uses this declaration.
- AffineMap.lineMap_apply_zeroproof · cited by 40
- neg_vadd_vaddproof · cited by 34
- vadd_neg_vaddproof · cited by 31
- IsAddQuotientCoveringMap.isCoveringMapproof · cited by 16
- AddAction.mem_orbit_selfproof · cited by 10
- collinear_pairproof · cited by 8
- vadd_zero_vaddproof · cited by 8
- Finset.affineCombination_of_eq_one_of_eq_zeroproof · cited by 8
- Collinear.mem_affineSpan_of_mem_of_neproof · cited by 7
- EuclideanGeometry.inversion_selfproof · cited by 6
- AffineMap.lineMap_same_applyproof · cited by 5
- Finset.card_inter_vaddproof · cited by 5