sub_add_vsub_comm — Mathlib

English

Let G be an abelian group acting on P by translations (a G-torsor). For all v1, v2 in G and p1, p2 in P, (v1 − v2) + (p1 −ᵥ p2) = (v1 +ᵥ p1) −ᵥ (v2 +ᵥ p2).

Русский

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

LaTeX

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

Lean4

theorem sub_add_vsub_comm (v₁ v₂ : G) (p₁ p₂ : P) : (v₁ - v₂) + (p₁ -ᵥ p₂) = (v₁ +ᵥ p₁) -ᵥ (v₂ +ᵥ p₂) :=
  vadd_vsub_vadd_comm _ _ _ _ |>.symm

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