Theorems · Theorem · group theory
vsub_vadd_eq_vsub_sub
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P) (g : G),
p₁ -ᵥ (g +ᵥ p₂) = p₁ -ᵥ p₂ - gSubtracting the result of adding a group element produces the same result as subtracting the points and subtracting that group element.
- Defined in
- Mathlib.Algebra.Torsor.Defs
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 13 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddstatement and proof · cited by 1,820
- AddTorsorstatement and proof · cited by 1,657
- VSub.vsubstatement and proof · cited by 817
- zero_subproof · cited by 335
- neg_add_cancelproof · cited by 256
- neg_vsub_eq_vsub_revproof · cited by 87
- add_sub_assocproof · cited by 72
- add_right_injproof · cited by 71
- vadd_vsubproof · cited by 58
- vsub_add_vsub_cancelproof · cited by 41
Cited by32
Results whose statement or proof uses this declaration.
- direction_affineSpanproof · cited by 46
- vsub_sub_vsub_cancel_rightproof · cited by 39
- vadd_vsub_vadd_cancel_rightproof · cited by 9
- Sbtw.angle₁₂₃_eq_piproof · cited by 6
- AffineSubspace.wSameSide_iff_exists_leftproof · cited by 5
- Wbtw.wOppSide₁₃proof · cited by 4
- vadd_vsub_vadd_cancel_leftproof · cited by 4
- Wbtw.trans_left_rightproof · cited by 3
- AffineSubspace.mem_affineSpan_insert_iffproof · cited by 3
- AffineSubspace.wOppSide_vadd_left_iffproof · cited by 2
- Affine.Simplex.points_vsub_eulerPointproof · cited by 2
- AffineSubspace.wSameSide_vadd_left_iffproof · cited by 2