vadd_right_cancel — Mathlib

English

If g1 +ᵥ p = g2 +ᵥ p for some p ∈ P, then g1 = g2.

Русский

Если для некоторого p ∈ P верно g1 +ᵥ p = g2 +ᵥ p, то g1 = g2.

LaTeX

$$$$ g_1 +_{v} p = g_2 +_{v} p \Rightarrow g_1 = g_2 $$$$

Lean4

/-- If the same point added to two group elements produces equal
results, those group elements are equal. -/
theorem vadd_right_cancel {g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂ := by
  rw [← vadd_vsub g₁ p, h, vadd_vsub]

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