ne_one

Mathlib.GroupTheory.Perm.Cycle.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.IsCycle.ne_one

English

If f is IsCycle, then f is not the identity; in particular, 1 is not a cycle.

Русский

Если f — цикл, то f не является тождественной перестановкой; в частности, 1 не является циклом.

LaTeX

$$IsCycle f → f ≠ 1$$

Lean4

theorem ne_one (h : IsCycle f) : f ≠ 1 := fun hf => by simp [hf, IsCycle] at h

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

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

Разделы

Аффилиация

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