swap_eq_one_iff

Mathlib.Algebra.Group.End

URI: https://scilib.ai/kg/mathlib#Equiv.swap_eq_one_iff

English

A swap is the identity permutation if and only if the swapped elements are equal.

Русский

Обмен равен единице тогда и только тогда, когда swapped элементы равны.

LaTeX

$$$ \\mathrm{swap}(i,j) = 1 \\iff i = j $$$

Lean4

@[simp]
theorem swap_eq_one_iff {i j : α} : swap i j = (1 : Perm α) ↔ i = j :=
  swap_eq_refl_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru