cycleRange_mk_zero — Mathlib

English

If n > 0 and we take the zero element of Fin n, its cycleRange is the identity permutation.

Русский

Если n > 0 и взять нулевой элемент Fin n, то его cycleRange является тождественной перестановкой.

LaTeX

$$$\operatorname{cycleRange}(\langle 0, h\rangle) = 1$,\quad h: 0 < n$$

Lean4

@[simp]
theorem cycleRange_mk_zero (h : 0 < n) : cycleRange ⟨0, h⟩ = 1 :=
  have : NeZero n := .of_pos h
  cycleRange_zero n

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