Theorems · Theorem · group theory

vadd_vsub_assoc

∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p₁ p₂ : P),
  (g +ᵥ p₁) -ᵥ p₂ = g + (p₁ -ᵥ p₂)

Adding a group element to a point, then subtracting another point, produces the same result as subtracting the points then adding the group element.

Defined in

Mathlib.Algebra.Torsor.Defs

Cited by

40 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

AddGroupAddTorsor