finRotate_symm_lt_iff_ne_zero — Mathlib

English

For [NeZero n] and i ∈ Fin n, ((finRotate n).symm i) < i iff i ≠ 0.

Русский

Для [NeZero n] и i ∈ Fin n: (finRotate n).symm i < i тогда, когда i ≠ 0.

LaTeX

$$$ i \\in \\mathrm{Fin}(n) \\Rightarrow (\\mathrm{finRotate}(n)).symm i < i \\iff i \\neq 0 $$$

Lean4

theorem finRotate_symm_lt_iff_ne_zero [NeZero n] (i : Fin n) : (finRotate _).symm i < i ↔ i ≠ 0 :=
  by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  refine ⟨fun hi hc ↦ ?_, fun hi ↦ ?_⟩
  · simp only [hc, Fin.not_lt_zero] at hi
  · rw [Fin.lt_iff_val_lt_val, coe_finRotate_symm_of_ne_zero hi]
    apply sub_lt (zero_lt_of_ne_zero <| Fin.val_ne_zero_iff.mpr hi) Nat.zero_lt_one

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