rfl

Mathlib.GroupTheory.Perm.Cycle.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.SameCycle.rfl

English

For any permutation f and any x, f.SameCycle x x holds (reflexivity).

Русский

Для любой перестановки f и любого x выполняется f.SameCycle x x (рефлексивность).

LaTeX

$$theorem SameCycle.refl (f : Perm α) (x : α) : SameCycle f x x$$

Lean4

theorem rfl : SameCycle f x x :=
  SameCycle.refl _ _

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

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

Разделы

Аффилиация

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