lt_finRotate_iff_ne_neg_one — Mathlib

English

For [NeZero n], and i ∈ Fin n, i < finRotate n i iff i ≠ -1.

Русский

При [NeZero n] и i ∈ Fin n: i < finRotate n i тогда, когда i ≠ -1.

LaTeX

$$$ i < \\mathrm{finRotate}(n)\\, i \\iff i \\neq -1 $$$

Lean4

theorem lt_finRotate_iff_ne_neg_one [NeZero n] (i : Fin n) : i < finRotate _ i ↔ i ≠ -1 :=
  by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [lt_finRotate_iff_ne_last, ne_eq, not_iff_not, ← Fin.neg_last, neg_neg]

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