symm_divLeft — Mathlib

English

In a commutative group, the left-division by a is its own inverse, i.e., divLeft a is its own inverse map.

Русский

В коммутативной группе деление слева на a является своей собственной обратной биекцией: divLeft a является инволютивной перестановкой.

LaTeX

$$$\\mathrm{divLeft}(a)^{-1} = \\mathrm{divLeft}(a)$ (in a commutative group)$$

Lean4

@[to_additive]
theorem symm_divLeft (a : G) : (Equiv.divLeft a).symm = Equiv.divLeft a :=
  ext fun _ ↦ inv_mul_eq_div _ _

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