val_sub_one_of_ne_zero — Mathlib

English

If i ≠ 0, then (i−1).val = i−1.

Русский

Если i ≠ 0, то (i−1).val = i−1.

LaTeX

$$$$\forall n:\\mathbb{N},\forall i:\\mathrm{Fin}(n), i\neq 0 \Rightarrow (i-1).\mathrm{val} = i-1.$$$$

Lean4

theorem val_sub_one_of_ne_zero [NeZero n] {i : Fin n} (hi : i ≠ 0) : (i - 1).val = i - 1 :=
  by
  obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (NeZero.ne n)
  rw [Fin.sub_val_of_le (one_le_of_ne_zero hi), Fin.val_one',
    Nat.mod_eq_of_lt (Nat.succ_le_iff.mpr (nontrivial_iff_two_le.mp <| nontrivial_of_ne i 0 hi))]

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