vsub_vadd_comm — Mathlib

English

Let P be a G-torsor with G abelian. For all p1, p2, p3 in P, (p1 −ᵥ p2) +ᵥ p3 = (p3 −ᵥ p2) +ᵥ p1.

Русский

Пусть P является торсером G с абелевой группой G. Тогда для любых p1, p2, p3 ∈ P выполняется (p1 −ᵥ p2) +ᵥ p3 = (p3 −ᵥ p2) +ᵥ p1.

LaTeX

$$$ (p_1 -_{\!v} p_2) +_{\!v} p_3 = (p_3 -_{\!v} p_2) +_{\!v} p_1 $$$

Lean4

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

Похожие утверждения