coe_finRotate_symm_of_ne_zero — Mathlib

English

For [NeZero n], and i : Fin n with i ≠ 0, the image under finRotate is i − 1 (in Nat form).

Русский

Для [NeZero n], i ∈ Fin n и i ≠ 0: образ finRotate равен i − 1 (в натуральном числе).

LaTeX

$$$ [\\mathrm{NeZero}\\ n] \\; (i : \\mathrm{Fin}(n)) \\; (i \\neq 0) \\Rightarrow ((\\mathrm{finRotate}(n))\\, i) = i - 1 $$$

Lean4

theorem coe_finRotate_symm_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) : ((finRotate _).symm i : ℕ) = i - 1 :=
  by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rwa [finRotate_succ_symm_apply, Fin.val_sub_one_of_ne_zero]

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