Mathlib.Algebra.AddTorsor.Basic

Set.singleton_vsub_self theorem

(p : P) : ({ p } : Set P) -ᵥ { p } = {(0 : G)}

Full source

theorem singleton_vsub_self (p : P) : ({p} : Set P) -ᵥ {p} = {(0 : G)} := by
  rw [Set.singleton_vsub_singleton, vsub_self]

Singleton Set Subtraction Yields Zero: $\{p\} -ᵥ \{p\} = \{0\}$

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the set subtraction of the singleton set $\{p\}$ from itself yields the singleton set containing the zero element of $G$, i.e., $\{p\} -ᵥ \{p\} = \{0\}$.

vsub_left_cancel theorem

{p₁ p₂ p : P} (h : p₁ -ᵥ p = p₂ -ᵥ p) : p₁ = p₂

Full source

/-- If the same point subtracted from two points produces equal
results, those points are equal. -/
theorem vsub_left_cancel {p₁ p₂ p : P} (h : p₁ -ᵥ p = p₂ -ᵥ p) : p₁ = p₂ := by
  rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h

Left Cancellation Property for Difference Vectors in Additive Torsor: $p_1 -ᵥ p = p_2 -ᵥ p \implies p_1 = p_2$

Informal description

For any points $p_1, p_2, p$ in an additive torsor $P$ over an additive group $G$, if the difference vectors $p_1 -ᵥ p$ and $p_2 -ᵥ p$ are equal, then $p_1 = p_2$.

vsub_left_cancel_iff theorem

{p₁ p₂ p : P} : p₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂

Full source

/-- The same point subtracted from two points produces equal results
if and only if those points are equal. -/
@[simp]
theorem vsub_left_cancel_iff {p₁ p₂ p : P} : p₁ -ᵥ pp₁ -ᵥ p = p₂ -ᵥ p ↔ p₁ = p₂ :=
  ⟨vsub_left_cancel, fun h => h ▸ rfl⟩

Equivalence of Point Equality and Difference Vector Equality in Additive Torsor: $p_1 -ᵥ p = p_2 -ᵥ p \leftrightarrow p_1 = p_2$

Informal description

For any points $p_1, p_2, p$ in an additive torsor $P$ over an additive group $G$, the difference vectors $p_1 -ᵥ p$ and $p_2 -ᵥ p$ are equal if and only if $p_1 = p_2$.

vsub_left_injective theorem

(p : P) : Function.Injective ((· -ᵥ p) : P → G)

Full source

/-- Subtracting the point `p` is an injective function. -/
theorem vsub_left_injective (p : P) : Function.Injective ((· -ᵥ p) : P → G) := fun _ _ =>
  vsub_left_cancel

Injectivity of Point Subtraction in Additive Torsor

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the function that subtracts $p$ from another point, i.e., $(\cdot -ᵥ p) : P \to G$, is injective. In other words, for any points $p_1, p_2 \in P$, if $p_1 -ᵥ p = p_2 -ᵥ p$, then $p_1 = p_2$.

vsub_right_cancel theorem

{p₁ p₂ p : P} (h : p -ᵥ p₁ = p -ᵥ p₂) : p₁ = p₂

Full source

/-- If subtracting two points from the same point produces equal
results, those points are equal. -/
theorem vsub_right_cancel {p₁ p₂ p : P} (h : p -ᵥ p₁ = p -ᵥ p₂) : p₁ = p₂ := by
  refine vadd_left_cancel (p -ᵥ p₂) ?_
  rw [vsub_vadd, ← h, vsub_vadd]

Right Cancellation Property for Torsor Subtraction

Informal description

For any points $p_1, p_2, p$ in an additive torsor $P$ over an additive group $G$, if the difference vectors $p -ᵥ p_1$ and $p -ᵥ p_2$ are equal, then $p_1 = p_2$.

vsub_right_cancel_iff theorem

{p₁ p₂ p : P} : p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂

Full source

/-- Subtracting two points from the same point produces equal results
if and only if those points are equal. -/
@[simp]
theorem vsub_right_cancel_iff {p₁ p₂ p : P} : p -ᵥ p₁p -ᵥ p₁ = p -ᵥ p₂ ↔ p₁ = p₂ :=
  ⟨vsub_right_cancel, fun h => h ▸ rfl⟩

Right Cancellation Property for Torsor Subtraction (iff form)

Informal description

For any points $p_1, p_2, p$ in an additive torsor $P$ over an additive group $G$, the difference vectors $p -ᵥ p_1$ and $p -ᵥ p_2$ are equal if and only if $p_1 = p_2$.

vsub_right_injective theorem

(p : P) : Function.Injective ((p -ᵥ ·) : P → G)

Full source

/-- Subtracting a point from the point `p` is an injective
function. -/
theorem vsub_right_injective (p : P) : Function.Injective ((p -ᵥ ·) : P → G) := fun _ _ =>
  vsub_right_cancel

Injectivity of Point Subtraction in Additive Torsor

Informal description

For any point $p$ in an additive torsor $P$ over an additive group $G$, the function that subtracts $p$ from another point, i.e., the map $q \mapsto p -ᵥ q$ from $P$ to $G$, is injective.

vsub_sub_vsub_cancel_left theorem

(p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂

Full source

/-- Cancellation subtracting the results of two subtractions. -/
@[simp]
theorem vsub_sub_vsub_cancel_left (p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂ := by
  rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]

Left Cancellation of Chained Difference Vectors in Additive Torsor

Informal description

For any three points $p_1, p_2, p_3$ in an additive torsor $P$ over an additive group $G$, the difference between the vectors $(p_3 -ᵥ p_2)$ and $(p_3 -ᵥ p_1)$ equals the vector $(p_1 -ᵥ p_2)$, i.e., $$(p_3 -ᵥ p_2) - (p_3 -ᵥ p_1) = p_1 -ᵥ p_2.$$

vadd_vsub_vadd_cancel_left theorem

(v : G) (p₁ p₂ : P) : (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂

Full source

@[simp]
theorem vadd_vsub_vadd_cancel_left (v : G) (p₁ p₂ : P) : (v +ᵥ p₁) -ᵥ (v +ᵥ p₂) = p₁ -ᵥ p₂ := by
  rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel_left]

Translation Invariance of Difference Vectors in Additive Torsor: $(v +ᵥ p_1) -ᵥ (v +ᵥ p_2) = p_1 -ᵥ p_2$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group element $v \in G$ and points $p_1, p_2 \in P$, the difference vector between the translated points $v +ᵥ p_1$ and $v +ᵥ p_2$ equals the difference vector $p_1 -ᵥ p_2$, i.e., $$(v +ᵥ p_1) -ᵥ (v +ᵥ p_2) = p_1 -ᵥ p_2.$$

vsub_vadd_comm theorem

(p₁ p₂ p₃ : P) : (p₁ -ᵥ p₂ : G) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁

Full source

theorem vsub_vadd_comm (p₁ p₂ p₃ : P) : (p₁ -ᵥ p₂ : G) +ᵥ p₃ = (p₃ -ᵥ p₂) +ᵥ p₁ := by
  rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]
  simp

Commutativity of Difference Vector Action in Additive Torsor: $(p_1 -ᵥ p₂) +ᵥ p_3 = (p_3 -ᵥ p₂) +ᵥ p_1$

Informal description

For any three points $p_1, p_2, p_3$ in an additive torsor $P$ over an additive group $G$, the action of the difference vector $(p_1 -ᵥ p₂)$ on $p_3$ equals the action of the difference vector $(p_3 -ᵥ p₂)$ on $p_1$, i.e., $$(p_1 -ᵥ p₂) +ᵥ p_3 = (p_3 -ᵥ p₂) +ᵥ p_1.$$

vadd_eq_vadd_iff_sub_eq_vsub theorem

{v₁ v₂ : G} {p₁ p₂ : P} : v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂

Full source

theorem vadd_eq_vadd_iff_sub_eq_vsub {v₁ v₂ : G} {p₁ p₂ : P} :
    v₁ +ᵥ p₁v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂ := by
  rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]

Equality of Translated Points in Additive Torsor via Difference: $v_1 +ᵥ p_1 = v_2 +ᵥ p_2 \leftrightarrow v_2 - v_1 = p_1 -ᵥ p_2$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group elements $v_1, v_2 \in G$ and points $p_1, p_2 \in P$, the equality $v_1 +ᵥ p_1 = v_2 +ᵥ p_2$ holds if and only if $v_2 - v_1 = p_1 -ᵥ p_2$.

vsub_sub_vsub_comm theorem

(p₁ p₂ p₃ p₄ : P) : p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)

Full source

theorem vsub_sub_vsub_comm (p₁ p₂ p₃ p₄ : P) : p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄) := by
  rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]

Commutativity of Difference Vector Subtraction in Additive Torsor

Informal description

For any four points $p_1, p_2, p_3, p_4$ in an additive torsor $P$ over an additive group $G$, the following equality holds: $$(p_1 -ᵥ p_2) - (p_3 -ᵥ p_4) = (p_1 -ᵥ p_3) - (p_2 -ᵥ p_4).$$

Set.vadd_set_vsub_vadd_set theorem

(v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t

Full source

@[simp] lemma vadd_set_vsub_vadd_set (v : G) (s t : Set P) : (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t := by
  ext; simp [mem_vsub, mem_vadd_set]

Translation Invariance of Difference Sets in Additive Torsor: $(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t$

Informal description

Let $G$ be an additive group acting on a torsor $P$. For any group element $v \in G$ and subsets $s, t \subseteq P$, the difference set between the translated sets $v +ᵥ s$ and $v +ᵥ t$ equals the difference set $s -ᵥ t$, i.e., $$(v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t.$$

Prod.instAddTorsor instance

: AddTorsor (G × G') (P × P')

Full source

instance instAddTorsor : AddTorsor (G × G') (P × P') where
  vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)
  zero_vadd _ := Prod.ext (zero_vadd _ _) (zero_vadd _ _)
  add_vadd _ _ _ := Prod.ext (add_vadd _ _ _) (add_vadd _ _ _)
  vsub p₁ p₂ := (p₁.1 -ᵥ p₂.1, p₁.2 -ᵥ p₂.2)
  vsub_vadd' _ _ := Prod.ext (vsub_vadd _ _) (vsub_vadd _ _)
  vadd_vsub' _ _ := Prod.ext (vadd_vsub _ _) (vadd_vsub _ _)

Product of Additive Torsors is an Additive Torsor

Informal description

For any two additive torsors $(G, P)$ and $(G', P')$, the product $G \times G'$ acts on the product $P \times P'$ in a natural way, making $P \times P'$ an additive torsor over $G \times G'$.

Prod.fst_vadd theorem

(v : G × G') (p : P × P') : (v +ᵥ p).1 = v.1 +ᵥ p.1

Full source

@[simp]
theorem fst_vadd (v : G × G') (p : P × P') : (v +ᵥ p).1 = v.1 +ᵥ p.1 :=
  rfl

First Component of Torsor Action on Product Space

Informal description

For any pair of group elements $v = (v_1, v_2) \in G \times G'$ and any pair of points $p = (p_1, p_2) \in P \times P'$ in the product torsor, the first component of the action $v +ᵥ p$ is equal to the action of the first component $v_1$ on the first component $p_1$, i.e., $(v +ᵥ p)_1 = v_1 +ᵥ p_1$.

Prod.snd_vadd theorem

(v : G × G') (p : P × P') : (v +ᵥ p).2 = v.2 +ᵥ p.2

Full source

@[simp]
theorem snd_vadd (v : G × G') (p : P × P') : (v +ᵥ p).2 = v.2 +ᵥ p.2 :=
  rfl

Second Component Preservation in Product Torsor Action

Informal description

For any pair of group elements $v = (v_1, v_2) \in G \times G'$ and any pair of points $p = (p_1, p_2) \in P \times P'$ in the product torsor, the second component of the action $v +ᵥ p$ is equal to the action of the second component of $v$ on the second component of $p$, i.e., $(v +ᵥ p)_2 = v_2 +ᵥ p_2$.

Prod.mk_vadd_mk theorem

(v : G) (v' : G') (p : P) (p' : P') : (v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')

Full source

@[simp]
theorem mk_vadd_mk (v : G) (v' : G') (p : P) (p' : P') : (v, v')(v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p') :=
  rfl

Componentwise Action in Product Torsor

Informal description

For any elements $v \in G$, $v' \in G'$ and points $p \in P$, $p' \in P'$, the action of $(v, v')$ on $(p, p')$ is given by $(v, v') +ᵥ (p, p') = (v +ᵥ p, v' +ᵥ p')$.

Prod.fst_vsub theorem

(p₁ p₂ : P × P') : (p₁ -ᵥ p₂ : G × G').1 = p₁.1 -ᵥ p₂.1

Full source

@[simp]
theorem fst_vsub (p₁ p₂ : P × P') : (p₁ -ᵥ p₂ : G × G').1 = p₁.1 -ᵥ p₂.1 :=
  rfl

First Component of Difference in Product Torsor

Informal description

For any two points $p_1 = (p_1^1, p_1^2)$ and $p_2 = (p_2^1, p_2^2)$ in the product torsor $P \times P'$, the first component of their difference $p_1 -ᵥ p_2$ in the group $G \times G'$ is equal to the difference $p_1^1 -ᵥ p_2^1$ in the first component group $G$.

Prod.snd_vsub theorem

(p₁ p₂ : P × P') : (p₁ -ᵥ p₂ : G × G').2 = p₁.2 -ᵥ p₂.2

Full source

@[simp]
theorem snd_vsub (p₁ p₂ : P × P') : (p₁ -ᵥ p₂ : G × G').2 = p₁.2 -ᵥ p₂.2 :=
  rfl

Second Component of Difference in Product Torsor

Informal description

For any two points $p_1 = (p_1^1, p_1^2)$ and $p_2 = (p_2^1, p_2^2)$ in the product torsor $P \times P'$, the second component of their difference vector $(p_1 -_{\cdot} p_2 : G \times G')$ is equal to the difference $p_1^2 -_{\cdot} p_2^2$ in the second torsor $P'$.

Prod.mk_vsub_mk theorem

(p₁ p₂ : P) (p₁' p₂' : P') : ((p₁, p₁') -ᵥ (p₂, p₂') : G × G') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂')

Full source

@[simp]
theorem mk_vsub_mk (p₁ p₂ : P) (p₁' p₂' : P') :
    ((p₁, p₁')(p₁, p₁') -ᵥ (p₂, p₂') : G × G') = (p₁ -ᵥ p₂, p₁' -ᵥ p₂') :=
  rfl

Difference of Pairs in Product Torsor Equals Pair of Differences

Informal description

For any points $p_1, p_2$ in an additive torsor $P$ and points $p_1', p_2'$ in an additive torsor $P'$, the difference between the pairs $(p_1, p_1')$ and $(p_2, p_2')$ in the product torsor $P \times P'$ is equal to the pair of differences $(p_1 - p_2, p_1' - p_2')$ in the product group $G \times G'$.

Pi.instAddTorsor instance

[∀ i, AddTorsor (fg i) (fp i)] : AddTorsor (∀ i, fg i) (∀ i, fp i)

Full source

/-- A product of `AddTorsor`s is an `AddTorsor`. -/
instance instAddTorsor [∀ i, AddTorsor (fg i) (fp i)] : AddTorsor (∀ i, fg i) (∀ i, fp i) where
  vadd g p i := g i +ᵥ p i
  zero_vadd p := funext fun i => zero_vadd (fg i) (p i)
  add_vadd g₁ g₂ p := funext fun i => add_vadd (g₁ i) (g₂ i) (p i)
  vsub p₁ p₂ i := p₁ i -ᵥ p₂ i
  vsub_vadd' p₁ p₂ := funext fun i => vsub_vadd (p₁ i) (p₂ i)
  vadd_vsub' g p := funext fun i => vadd_vsub (g i) (p i)

Product of Additive Torsors is an Additive Torsor

Informal description

For any family of additive torsors $(G_i, P_i)$ indexed by $i$, the product space $\prod_i P_i$ is an additive torsor over the product group $\prod_i G_i$.

Equiv.constVAdd_zero theorem

: constVAdd P (0 : G) = 1

Full source

@[simp]
theorem constVAdd_zero : constVAdd P (0 : G) = 1 :=
  ext <| zero_vadd G

Identity Permutation via Zero Vector Addition in Torsors

Informal description

For any additive torsor $(G, P)$, the permutation of $P$ induced by adding the zero element of $G$ is the identity permutation, i.e., $\text{constVAdd}_P(0) = 1$.

Equiv.constVAdd_add theorem

(v₁ v₂ : G) : constVAdd P (v₁ + v₂) = constVAdd P v₁ * constVAdd P v₂

Full source

@[simp]
theorem constVAdd_add (v₁ v₂ : G) : constVAdd P (v₁ + v₂) = constVAdd P v₁ * constVAdd P v₂ :=
  ext <| add_vadd v₁ v₂

Additivity of Constant Vector Addition Permutation: $\text{constVAdd}_P(v_1 + v_2) = \text{constVAdd}_P(v_1) \circ \text{constVAdd}_P(v_2)$

Informal description

For any two elements $v_1$ and $v_2$ of an additive group $G$ acting on a type $P$, the permutation obtained by adding $v_1 + v_2$ to each point in $P$ is equal to the composition of the permutations obtained by adding $v_1$ and $v_2$ separately. In other words, the map $\text{constVAdd}_P(v_1 + v_2)$ is equal to the product $\text{constVAdd}_P(v_1) \circ \text{constVAdd}_P(v_2)$.

Equiv.constVAddHom definition

: Multiplicative G →* Equiv.Perm P

Full source

/-- `Equiv.constVAdd` as a homomorphism from `Multiplicative G` to `Equiv.perm P` -/
def constVAddHom : MultiplicativeMultiplicative G →* Equiv.Perm P where
  toFun v := constVAdd P (v.toAdd)
  map_one' := constVAdd_zero G P
  map_mul' := constVAdd_add P

Homomorphism from additive group to permutation group via constant vector addition

Informal description

The function `Equiv.constVAddHom` is a monoid homomorphism from the multiplicative group `Multiplicative G` to the permutation group `Equiv.Perm P` of a type `P`. It maps each element `v` of `G` (viewed multiplicatively) to the permutation `constVAdd P v` of `P`, which translates each point in `P` by `v`. The homomorphism satisfies: 1. The identity element of `Multiplicative G` maps to the identity permutation (`constVAdd P 0 = 1`). 2. The product of two elements in `Multiplicative G` maps to the composition of their corresponding permutations (`constVAdd P (v₁ + v₂) = constVAdd P v₁ ∘ constVAdd P v₂`).

Equiv.left_vsub_pointReflection theorem

(x y : P) : x -ᵥ pointReflection x y = y -ᵥ x

Full source

@[simp]
theorem left_vsub_pointReflection (x y : P) : x -ᵥ pointReflection x y = y -ᵥ x :=
  neg_injective <| by simp

Left Difference Identity for Point Reflection: $x -ᵥ \text{pointReflection}(x, y) = y -ᵥ x$

Informal description

For any points $x$ and $y$ in an additive torsor $P$ over an additive group $G$, the difference vector from $x$ to the point reflection of $y$ about $x$ equals the difference vector from $y$ to $x$, i.e., $$x -ᵥ \text{pointReflection}(x, y) = y -ᵥ x.$$

Equiv.right_vsub_pointReflection theorem

(x y : P) : y -ᵥ pointReflection x y = 2 • (y -ᵥ x)

Full source

@[simp]
theorem right_vsub_pointReflection (x y : P) : y -ᵥ pointReflection x y = 2 • (y -ᵥ x) :=
  neg_injective <| by simp [← neg_nsmul]

Point Reflection Difference Identity: $y -ᵥ \text{pointReflection}\, x\, y = 2 \cdot (y -ᵥ x)$

Informal description

For any points $x, y$ in an additive torsor $P$ over an additive group $G$, the difference vector from $y$ to the point reflection of $y$ at $x$ is equal to twice the difference vector from $y$ to $x$, i.e., $$y -ᵥ \text{pointReflection}\, x\, y = 2 \cdot (y -ᵥ x).$$

Equiv.pointReflection_fixed_iff_of_injective_two_nsmul theorem

{x y : P} (h : Injective (2 • · : G → G)) : pointReflection x y = y ↔ y = x

Full source

/-- `x` is the only fixed point of `pointReflection x`. This lemma requires
`x + x = y + y ↔ x = y`. There is no typeclass to use here, so we add it as an explicit argument. -/
theorem pointReflection_fixed_iff_of_injective_two_nsmul {x y : P} (h : Injective (2 • · : G → G)) :
    pointReflectionpointReflection x y = y ↔ y = x := by
  rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
    neg_eq_iff_add_eq_zero, ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]

Fixed Points of Point Reflection in Torsors with Injective Doubling

Informal description

Let $G$ be an additive group acting on a torsor $P$, and suppose the map $g \mapsto 2 \cdot g$ is injective on $G$. For any points $x, y \in P$, the point reflection of $y$ about $x$ fixes $y$ if and only if $y = x$. That is, $\text{pointReflection}_x(y) = y \leftrightarrow y = x$.

Equiv.injective_pointReflection_left_of_injective_two_nsmul theorem

 {G P : Type*} [AddCommGroup G] [AddTorsor G P] (h : Injective (2 • · : G → G)) (y : P) :
  Injective fun x : P => pointReflection x y

Full source

theorem injective_pointReflection_left_of_injective_two_nsmul {G P : Type*} [AddCommGroup G]
    [AddTorsor G P] (h : Injective (2 • · : G → G)) (y : P) :
    Injective fun x : P => pointReflection x y :=
  fun x₁ x₂ (hy : pointReflection x₁ y = pointReflection x₂ y) => by
  rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy

Injectivity of Point Reflection in Torsors with Injective Doubling

Informal description

Let $G$ be an additive commutative group acting on an additive torsor $P$, and suppose the doubling map $g \mapsto 2 \cdot g$ is injective on $G$. Then for any fixed point $y \in P$, the function $x \mapsto \text{pointReflection}_x(y)$ is injective.