divLeft_involutive — Mathlib

English

For any a in a commutative group G, the map x ↦ x div a is an involution on G.

Русский

Для любого a в коммутативной группе G отображение x ↦ x / a является инволютивной перестановкой.

LaTeX

$$$\\text{Function.Involutive}(\\mathrm{divLeft}(a))$$$

Lean4

@[to_additive (attr := simp)]
theorem divLeft_involutive (a : G) : Function.Involutive (Equiv.divLeft a) := fun _ ↦ div_div_cancel ..

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