swap_mul_involutive — Mathlib

English

The map x ↦ x · swap i j is an involution; applying it twice yields the original element.

Русский

Отображение x ↦ x · swap i j является инволюцией; два раза применение возвращает исходное.

LaTeX

$$$ \\text{Involutive}(x \\mapsto x \\cdot \\mathrm{swap}(i,j)) $$$

Lean4

/-- A stronger version of `mul_right_injective` -/
@[simp]
theorem swap_mul_involutive (i j : α) : Function.Involutive (Equiv.swap i j * ·) :=
  swap_mul_self_mul i j

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