Theorems · Theorem · group theory
vadd_vsub
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p : P), (g +ᵥ p) -ᵥ p = gAdding a group element then subtracting the original point produces that group element.
- Defined in
- Mathlib.Algebra.Torsor.Defs
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 1,820
- AddTorsorstatement and proof · cited by 1,657
- VSub.vsubstatement · cited by 817
- AddTorsor.vadd_vsub'proof · cited by 1
Cited by59
Results whose statement or proof uses this declaration.
- vsub_selfproof · cited by 74
- vsub_vadd_eq_vsub_subproof · cited by 32
- AffineMap.linearMap_vsubproof · cited by 17
- eq_vadd_iff_vsub_eqproof · cited by 16
- AffineSubspace.direction_mk'proof · cited by 15
- AffineSubspace.direction_topproof · cited by 11
- dist_vadd_leftproof · cited by 9
- AffineMap.lineMap_vsub_leftproof · cited by 9
- AffineSubspace.vadd_mem_iff_mem_directionproof · cited by 9
- Equiv.vaddConstproof · cited by 8
- Collinear.mem_affineSpan_of_mem_of_neproof · cited by 7
- vadd_right_cancelproof · cited by 6