Theorems · Theorem · group theory
AddSemigroupAction.add_vadd
∀ {G : Type u_9} {P : Type u_10} {inst : AddSemigroup G} [self : AddSemigroupAction G P] (g₁ g₂ : G) (p : P),
(g₁ + g₂) +ᵥ p = g₁ +ᵥ g₂ +ᵥ pAssociativity of +ᵥ and +
- Defined in
- Mathlib.Algebra.Group.Action.Defs
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- AddSemigroupAction
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- HVAdd.hVAddstatement · cited by 1,820
- AddSemigroupstatement and proof · cited by 136
- AddSemigroupActionstatement and proof · cited by 3
Cited by43
Results whose statement or proof uses this declaration.
- vsub_add_vsub_cancelproof · cited by 41
- vadd_vaddproof · cited by 40
- vadd_vsub_assocproof · cited by 40
- EuclideanGeometry.reflection_apply'proof · cited by 6
- AffineSpace.asymptoticNhds_vadd_pureproof · cited by 5
- AddAction.nsmul_mod_period_vaddproof · cited by 3
- AddAction.zsmul_mod_period_vaddproof · cited by 3
- AddOreLocalization.oreSub_zero_surjective_of_finite_leftproof · cited by 2
- AddOreLocalization.oreSub_zero_surjective_of_finite_rightproof · cited by 2
- AddAction.mapsTo_vadd_orbitproof · cited by 2
- AffineEquiv.constVAdd_addproof · cited by 2
- wbtw_swap_left_iffproof · cited by 2