cycleRange_of_eq

Mathlib.GroupTheory.Perm.Fin

URI: https://scilib.ai/kg/mathlib#Fin.cycleRange_of_eq

English

If i = j, then (cycleRange j i) = 0.

Русский

Если i = j, то (cycleRange j i) = 0.

LaTeX

$$$ (\\mathrm{cycleRange}(j))(i) = 0 \\quad\\text{если } i=j$$$

Lean4

theorem cycleRange_of_eq [NeZero n] (h : i = j) : cycleRange j i = 0 := by rw [cycleRange_of_le h.le, if_pos h]

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

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

Разделы

Аффилиация

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