pointReflection_eq_subLeft — Mathlib

English

In additive commutative groups, pointReflection x equals subLeft (2x).

Русский

В абелевой группе точка отражения совпадает с операцией subLeft (2x).

LaTeX

$$$$ \text{pointReflection } x = \text{Equiv.subLeft} (2x) $$$$

Lean4

/-- In the special case of additive commutative groups (as opposed to just additive torsors),
`Equiv.pointReflection x` coincides with `Equiv.subLeft (2 • x)`. -/
theorem pointReflection_eq_subLeft {G : Type*} [AddCommGroup G] (x : G) : pointReflection x = Equiv.subLeft (2 • x) :=
  by ext; simp [pointReflection, sub_add_eq_add_sub, two_nsmul]

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