vsub_self
theorem vsub_self : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P), p -ᵥ p = 0 := by
sorry
This theorem states that for any point `p` in a given add torsor `P` over an add group `G`, subtracting `p` from itself yields the zero element of the add group `G`. This is a property of torsors in vector spaces: the difference between a point and itself is always the zero vector.
More concisely: For any point `p` in an add torsor `P` over an add group `G`, `p - p` equals the zero element of `G`.
|
vsub_add_vsub_cancel
theorem vsub_add_vsub_cancel :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P),
p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃
The theorem `vsub_add_vsub_cancel` states that for any three points `p₁`, `p₂`, and `p₃` belonging to an AddTorsor `P` over an AddGroup `G`, the vector difference of `p₁` and `p₂` added to the vector difference of `p₂` and `p₃` equals the vector difference of `p₁` and `p₃`. In simpler terms, it's saying that if you move from `p₂` to `p₁` and then from `p₂` to `p₃`, it's the same as just moving from `p₃` to `p₁` directly. This is essentially the cancellation law for this structure, in the context of subtraction and addition.
More concisely: For any points `p₁`, `p₂`, and `p₃` in an AddTorsor `P` over an AddGroup `G`, `(p₁ - p₂) + (p₂ - p₃) = p₁ - p₃`.
|
vsub_left_cancel_iff
theorem vsub_left_cancel_iff :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P},
p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂
This theorem states that for any given points `p₁`, `p₂`, and `p` in an additive torsor `P` over an additive group `G`, the vector from `p` to `p₁` is equal to the vector from `p` to `p₂` if and only if `p₁` is equal to `p₂`. In other words, if subtracting the same point `p` from two different points `p₁` and `p₂` yields the same result, then the points `p₁` and `p₂` must be the same.
More concisely: Given any additive torsor P over an additive group G and points p₁, p₂, and p in P, the vectors p₁ - p and p₂ - p are equal if and only if p₁ = p₂.
|
vadd_vsub_vadd_cancel_right
theorem vadd_vsub_vadd_cancel_right :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (v₁ v₂ : G) (p : P),
v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
This theorem states that for all types `G` and `P`, where `G` is an add group and `P` is an add torsor over `G`, and for all elements `v₁`, `v₂` of `G` and `p` of `P`, the result of adding `v₁` to `p` (denoted by `v₁ +ᵥ p`), subtracting the result of adding `v₂` to `p` (denoted by `v₂ +ᵥ p`), is equal to the subtraction of `v₂` from `v₁` (denoted by `v₁ - v₂`). Essentially, this theorem encapsulates the right cancellation law for addition and subtraction in the context of add torsors.
More concisely: For all add groups G and add torsors P over G, for all elements v₁, v₂ of G and p of P, the operation of adding an element v₁ to a torsor p and then subtracting an element v₂ gives the same result as subtracting v₂ from v₁ and adding the result to p. In symbols: v₁ +ᵥ p = (v₁ - v₂) +ᵥ p.
|
Mathlib.Algebra.AddTorsor._auxLemma.2
theorem Mathlib.Algebra.AddTorsor._auxLemma.2 :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P}, (p₁ -ᵥ p₂ = 0) = (p₁ = p₂)
This theorem, `Mathlib.Algebra.AddTorsor._auxLemma.2`, states that for any types `G` and `P`, where `G` is an additive group and `P` is an additive torsor over `G`, and for any two elements `p₁` and `p₂` of `P`, the difference `p₁ -ᵥ p₂` being equal to zero is equivalent to `p₁` being equal to `p₂`. In other words, in the context of additive torsors, subtracting one point from another and getting zero indicates that the two points are identical.
More concisely: In an additive torsor over an additive group, two elements are equal if and only if their difference is the zero element of the group.
|
vsub_eq_zero_iff_eq
theorem vsub_eq_zero_iff_eq :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P}, p₁ -ᵥ p₂ = 0 ↔ p₁ = p₂ := by
sorry
This theorem, denoted as `vsub_eq_zero_iff_eq`, states that for any two points `p₁` and `p₂` of type `P` in an additive torsor `T` over an additive group `G`, the vector subtraction of `p₁` and `p₂` equals zero if and only if `p₁` and `p₂` are equal. In other words, it establishes the equivalence between the condition of two points being identical and the resulting vector from their subtraction being a zero vector in the given torsor and group structure.
More concisely: For any additive torsor T over an additive group G and any points p₁, p₂ of type P in T, p₁ - p₂ = 0 if and only if p₁ = p₂.
|
vsub_vadd
theorem vsub_vadd :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P), p₁ -ᵥ p₂ +ᵥ p₂ = p₁
This theorem states that for any two points `p₁` and `p₂` in an additive group `G` with an associated add-torsor `T`, subtracting `p₂` from `p₁` (denoted by `p₁ -ᵥ p₂`) and then adding `p₂` back to the result (denoted by `(p₁ -ᵥ p₂) +ᵥ p₂`) gives us `p₁` back. Essentially, this is saying that adding the result of a subtraction from another point brings us back to the original point. This holds for all points in an additive torsor over an additive group.
More concisely: For all points `p₁` and `p₂` in an additive group `G` with an associated add-torsor, `p₁ -ᵥ p₂ +ᵥ p₂ = p₁`.
|
vsub_sub_vsub_cancel_left
theorem vsub_sub_vsub_cancel_left :
∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (p₁ p₂ p₃ : P),
p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂
This theorem states that for any three points `p₁`, `p₂`, and `p₃` in an additive torsor `P` over an additive commutative group `G`, the result of subtracting the subtraction of `p₃` and `p₂` from the subtraction of `p₃` and `p₁` equals the subtraction of `p₁` and `p₂`. In other words, it establishes a cancellation property of subtraction function `-ᵥ` in the context of an additive torsor.
More concisely: For any additive torsor P over an additive commutative group G and any points p₁, p₂, p₃ in P, we have p₁ − (p₃ − p₂) = p₁ − p₃ + p₂.
|
AddTorsor.vadd_vsub'
theorem AddTorsor.vadd_vsub' :
∀ {G : outParam (Type u_1)} {P : Type u_2} [inst : outParam (AddGroup G)] [self : AddTorsor G P] (g : G) (p : P),
g +ᵥ p -ᵥ p = g
The theorem `AddTorsor.vadd_vsub'` states that for any element `g` from an additive group `G` and any element `p` from a type `P` that is an additive torsor for `G`, the operation of adding `g` to `p` (using the torsor addition operation `+ᵥ`) and then subtracting `p` (using the torsor subtraction operation `-ᵥ`) results in the original element `g`. Essentially, it says that torsor addition and subtraction of the same element cancels out.
More concisely: For any additive group `G`, additive torsor `P` over `G`, and element `g` in `G`, we have `g +ᵥ p = p +ᵥ g`.
|
vsub_left_injective
theorem vsub_left_injective :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P),
Function.Injective fun x => x -ᵥ p
The theorem `vsub_left_injective` states that for any type `G` representing a group with addition (`AddGroup`), type `P` and an element `p` of this type `P` in which `P` is an additive torsor over `G` (`AddTorsor G P`), the function that subtracts the point `p` from any other point `x` (denoted as `x -ᵥ p`) is injective. In other words, if two points `x` and `y` in the torsor yield the same result when `p` is subtracted from them, then `x` and `y` must be the same point.
More concisely: For any additive torsor `P` over a group `G` and any elements `x, y` in `P`, if `x -ᵥ p = y -ᵥ p` for some `p` in `G`, then `x = y`.
|
eq_of_vsub_eq_zero
theorem eq_of_vsub_eq_zero :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ : P}, p₁ -ᵥ p₂ = 0 → p₁ = p₂ := by
sorry
This theorem asserts that in any additive group `G` with an associated torsor `P`, if the vector subtraction of two points `p₁` and `p₂` from `P` yields the zero element of the group, then the two points `p₁` and `p₂` must be equal. An additive torsor is a set with a free and transitive additive group action. This theorem is essentially a formalization of the geometric intuition that subtracting a point from itself in a vector space should yield the zero vector.
More concisely: In an additive group with a torsor structure, if the difference of two points in the torsor is the group's zero element, then the two points are equal.
|
vsub_right_injective
theorem vsub_right_injective :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P),
Function.Injective fun x => p -ᵥ x
The theorem `vsub_right_injective` states that for any given types `G` and `P` where `G` is an additive group and `P` is an additive torsor over `G`, subtracting any point from a fixed point `p` of type `P` is an injective function. In other words, if we have two points `x` and `y` in `P` such that `p -ᵥ x = p -ᵥ y`, then `x` must be equal to `y`.
More concisely: If `p` is a point in an additive torsor `P` over an additive group `G`, then the function `x mapsto p - x` is an injection from `P` to `G`.
|
AddTorsor.vsub_vadd'
theorem AddTorsor.vsub_vadd' :
∀ {G : outParam (Type u_1)} {P : Type u_2} [inst : outParam (AddGroup G)] [self : AddTorsor G P] (p₁ p₂ : P),
p₁ -ᵥ p₂ +ᵥ p₂ = p₁
The theorem `AddTorsor.vsub_vadd'` states that for any two elements `p₁` and `p₂` of a given type `P` in an additive torsor (a mathematical structure that generalizes vector spaces and affine spaces) over an additive group `G`, subtracting `p₂` from `p₁` (notated as `p₁ -ᵥ p₂`) and then adding `p₂` back results in `p₁`. In other words, in the context of an additive torsor, the operation of subtracting and then adding the same element cancels out, returning the original element.
More concisely: For any elements `p₁` and `p₂` in an additive torsor `P` over an additive group `G`, `p₁ -ᵥ p₂ + p₂ = p₁`.
|
vsub_left_cancel
theorem vsub_left_cancel :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P},
p₁ -ᵥ p = p₂ -ᵥ p → p₁ = p₂
This theorem states that for any type `G` with an `AddGroup` instance, any type `P` with an `AddTorsor` instance over `G`, and any three points `p₁`, `p₂`, and `p` of type `P`, if subtracting `p` from `p₁` and `p₂` (in the vector sense) results in equal values, then `p₁` and `p₂` must be equal. This theorem essentially asserts a property of subtraction in the context of torsors and groups: if the subtraction of the same value from two points gives the same result, then the two points must have been equal.
More concisely: If `p₁, p₂` are elements of a `AddTorsor` over an `AddGroup` `G`, then `p₁ - p = p₂ - p` implies `p₁ = p₂`.
|
vsub_eq_sub
theorem vsub_eq_sub : ∀ {G : Type u_1} [inst : AddGroup G] (g₁ g₂ : G), g₁ -ᵥ g₂ = g₁ - g₂
This theorem states that for any `AddGroup G` and any two elements `g₁` and `g₂` from `G`, the operation of "subtraction in the sense of torsors" (`g₁ -ᵥ g₂`) is equivalent to the standard subtraction operation (`g₁ - g₂`). Here, a torsor can be intuitively understood as a space that looks exactly like a given group, but doesn't have a designated "zero point". Its subtraction is defined in terms of the group operation, but without reference to any specific point.
More concisely: For any AddGroup G and elements g₁, g₂ from G, the subtraction in the sense of torsors g₁ -ᵥ g₂ equals the standard subtraction g₁ - g₂.
|
vsub_right_cancel_iff
theorem vsub_right_cancel_iff :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P},
p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂
This theorem states that for any given types `G` and `P`, where `G` forms an additive group and `P` is an additive torsor over `G`, subtracting two points (`p₁` and `p₂`) from the same point `p` (in the sense of the torsor operation) will yield equal results if and only if `p₁` and `p₂` are the same point. This can be seen as a cancellation law for the subtract operation in the context of torsors.
More concisely: For any additive torsors `P` over an additive group `G`, subtracting the same point from two points `p₁` and `p₂` in `P` yields equality: `p₁ - p = p₂ - p` if and only if `p₁ = p₂`.
|
vadd_right_cancel
theorem vadd_right_cancel :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {g₁ g₂ : G} (p : P),
g₁ +ᵥ p = g₂ +ᵥ p → g₁ = g₂
This theorem states that for any two elements (`g₁` and `g₂`) from an additive group `G` and a point `p` from a set `P` that forms an additive torsor with `G`, if adding the same point `p` to both `g₁` and `g₂` results in the same value, then `g₁` and `g₂` must be equal to each other. An additive group is a set equipped with an addition operation that is associative, commutative, has an identity element, and every element has an inverse. An additive torsor is a set that behaves like an additive group without an identity element, it is usually a set of "points" on which the group "acts".
More concisely: If `g₁` and `g₂` are elements of an additive group `G`, and `p` is a point in a set `P` forming an additive torsor with `G`, then `g₁ + p = g₂ + p` implies `g₁ = g₂`.
|
vsub_right_cancel
theorem vsub_right_cancel :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p₁ p₂ p : P},
p -ᵥ p₁ = p -ᵥ p₂ → p₁ = p₂
This theorem states that for any given types `G` and `P`, where `G` is an additive group, and `P` is an additive torsor over `G`, if you have three points `p`, `p₁`, and `p₂` of type `P`, then if the vector from `p₁` to `p` is equal to the vector from `p₂` to `p`, that implies `p₁` and `p₂` are the same point. In more mathematical terms, if $p - p₁ = p - p₂$, then $p₁ = p₂$.
More concisely: If `p₁`, `p`, and `p₂` are points of an additive torsor `P` over an additive group `G`, then `p₁ = p₂` if and only if `p - p₁ = p - p₂`.
|
vadd_vsub_assoc
theorem 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₂)
This theorem, `vadd_vsub_assoc`, states that for any additive group `G` and any torsor `P` over `G`, as well as any group element `g` and points `p₁` and `p₂` in `P`, adding `g` to `p₁` and then subtracting `p₂` yields the same result as first subtracting `p₂` from `p₁` and then adding `g`. In other words, it shows that vector addition followed by vector subtraction is associative in this context.
More concisely: For any additive group G and torsor P over G, for all g in G and p₁, p₂ in P, we have p₁ + g - p₂ = p₁ - p₂ + g.
|
Equiv.pointReflection_apply
theorem Equiv.pointReflection_apply :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x y : P),
(Equiv.pointReflection x) y = x -ᵥ y +ᵥ x
This theorem states that for any types G and P, given that G is an additive group and P is an additive torsor over G, the application of the point reflection operation at a point 'x' to another point 'y' results in the vector subtraction of 'y' from 'x' followed by vector addition to 'x'. In mathematical terms, `pointReflection(x)(y) = x - y + x`. The point reflection operation is established here as a function that reflects a point over another point in an additive group structure.
More concisely: For any additive group G and additive torsor P over G, point reflection of y in x is equivalent to subtracting y from x and adding x, that is, `pointReflection(x)(y) = x - y + x`.
|
vadd_vsub
theorem vadd_vsub :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p : P), g +ᵥ p -ᵥ p = g
This theorem states that for any group `G`, point `P` (with `G` acting on `P` in an additive manner), group element `g` in `G`, and point `p` in `P`, if you add `g` to `p` and then subtract `p`, the result will be `g`. This is analogous to the rule in ordinary arithmetic that (a + b) - b = a.
More concisely: For any group `G` acting additively on a set `P`, and for all `g` in `G` and `p` in `P`, the group operation satisfies `g + p - p = g`.
|
vadd_right_injective
theorem vadd_right_injective :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p : P),
Function.Injective fun x => x +ᵥ p
This theorem, `vadd_right_injective`, states that for any group `G` and any type `P` that forms an additive torsor over `G` (a set on which `G` acts freely and transitively), and for any point `p` in `P`, the function that adds an element of the group `G` to the point `p` (denoted as `x +ᵥ p`) is injective. In other words, if you have two different elements in the group `G`, they will map to two different points in `P` when added to `p`. This property holds for all `p` in `P`.
More concisely: For any group `G` and additive torsor `P` over `G`, the function `x mapsto x +ᵥ p` from `G` to `P` is an injection.
|
vsub_ne_zero
theorem vsub_ne_zero :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] {p q : P}, p -ᵥ q ≠ 0 ↔ p ≠ q
This theorem states that for any types `G` and `P`, where `G` has an addition group structure and `P` is an additive torsor over `G`, the difference between two points `p` and `q` of type `P` (represented as `p -ᵥ q`) is not zero if and only if `p` and `q` are not equal. In other words, in this context, two points are distinct if and only if their "vector difference" is non-zero.
More concisely: For any additive torsors `P` over an additive group `G`, two points `p` and `q` in `P` differ, i.e., `p -ᵥ q ≠ 0`, if and only if `p` and `q` are not equal.
|
Equiv.pointReflection_fixed_iff_of_injective_bit0
theorem Equiv.pointReflection_fixed_iff_of_injective_bit0 :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] {x y : P},
Function.Injective bit0 → ((Equiv.pointReflection x) y = y ↔ y = x)
The theorem `Equiv.pointReflection_fixed_iff_of_injective_bit0` asserts that for any types `G` and `P`, where `G` is an additive group and `P` is a torsor for `G`, and any points `x` and `y` of `P`, if the `bit0` function (which doubles its input) is injective, then `y` is a fixed point of the point reflection in `x` if and only if `y` equals `x`. In other words, `x` is the only fixed point of its own point reflection, provided that doubling a value gives a unique result.
More concisely: For any additive group `G` and its torsor `P`, if `bit0` is injective on `P`, then a point `y` in `P` is a fixed point of the point reflection in `x` if and only if `y` equals `x`.
|
vsub_vadd_eq_vsub_sub
theorem 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₂ - g
This theorem states that for any group `G` and any torsor `T` over that group, for any two points `p₁` and `p₂` in `T` and any element `g` in `G`, subtracting the result of adding `g` to `p₂` from `p₁` is the same as first subtracting `p₂` from `p₁` and then subtracting `g`. In mathematical terms, it's stating that \( p₁ - (g + p₂) = (p₁ - p₂) - g \) within the structure provided by the group and the torsor.
More concisely: For any group `G` and torsor `T` over `G`, for all `p₁`, `p₂` in `T` and `g` in `G`, `p₁ - g - p₂ = p₁ - p₂ - g`.
|
Equiv.pointReflection_involutive
theorem Equiv.pointReflection_involutive :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x : P),
Function.Involutive ⇑(Equiv.pointReflection x)
The theorem `Equiv.pointReflection_involutive` states that for any type `G` and `P`, where `G` has an additive group structure and `P` is an additive torsor over `G`, the point reflection operation at any point `x` of `P` is an involutive function. In other words, applying the point reflection operation twice returns the original point, which is equivalent to saying that the point reflection operation is its own inverse.
More concisely: For any additive group `G` and additive torsor `P` over `G`, the point reflection function on `P` is an involution.
|
eq_vadd_iff_vsub_eq
theorem eq_vadd_iff_vsub_eq :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ : P) (g : G) (p₂ : P),
p₁ = g +ᵥ p₂ ↔ p₁ -ᵥ p₂ = g
This theorem, `eq_vadd_iff_vsub_eq`, establishes a relationship between addition and subtraction in the context of an additive group and an associated torsor. Specifically, for any given types `G` and `P` where `G` is an additive group and `P` is a torsor over `G`, and for any individual elements `p₁`, `g` and `p₂`, it asserts that `p₁` being equal to `g` added to `p₂` is equivalent to the subtraction of `p₂` from `p₁` resulting in `g`.
More concisely: For any additive group `G` and torsor `P` over `G`, and for any elements `p₁`, `g`, and `p₂` in `G` and `P` respectively, `p₁ = g + p₂` if and only if `p₁ - p₂ = g`.
|
neg_vsub_eq_vsub_rev
theorem neg_vsub_eq_vsub_rev :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ : P), -(p₁ -ᵥ p₂) = p₂ -ᵥ p₁ := by
sorry
This theorem, `neg_vsub_eq_vsub_rev`, states that for any two points `p₁` and `p₂` in any `AddTorsor` space `P` over an `AddGroup` `G`, the negation of the subtraction of `p₁` from `p₂`, denoted as `-(p₁ -ᵥ p₂)`, is equal to the subtraction of `p₂` from `p₁`, denoted as `p₂ -ᵥ p₁`. This theorem is essentially a mathematical equivalent of the idea that reversing the order of subtraction is the same as taking the negative of the original subtraction.
More concisely: For any points `p₁` and `p₂` in an `AddTorsor` space `P` over an `AddGroup` `G`, `-(p₁ -ᵥ p₂) = p₂ -ᵥ p₁`.
|
vsub_sub_vsub_cancel_right
theorem vsub_sub_vsub_cancel_right :
∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (p₁ p₂ p₃ : P),
p₁ -ᵥ p₃ - (p₂ -ᵥ p₃) = p₁ -ᵥ p₂
This theorem, `vsub_sub_vsub_cancel_right`, states that for any three points `p₁`, `p₂`, and `p₃` in a torsor `P` over an additive group `G`, the difference between the subtraction of `p₃` from `p₁` and the subtraction of `p₃` from `p₂` is equal to the subtraction of `p₂` from `p₁`. In mathematical terms, it says that $(p₁ - p₃) - (p₂ - p₃) = p₁ - p₂$. It's a cancellation law for subtraction in the context of torsors.
More concisely: For any points `p₁`, `p₂`, `p₃` in a torsor `P` over an additive group `G`, the subtraction of `p₂` from `p₁` is equal to the difference between `p₁` and the difference of `p₁` and `p₃`. In symbols, `p₁ - (p₂ - p₃) = p₁ - p₂`.
|