Documentation

Mathlib.Init.Data.Fin.Basic

Theorems about equality in Fin. #

@[deprecated Fin.eq_of_val_eq]
theorem Fin.eq_of_veq {n : } {i : Fin n} {j : Fin n} :
i = ji = j
@[deprecated Fin.val_eq_of_eq]
theorem Fin.veq_of_eq {n : } {i : Fin n} {j : Fin n} :
i = ji = j
theorem Fin.ne_of_vne {n : } {i : Fin n} {j : Fin n} (h : i j) :
i j
theorem Fin.vne_of_ne {n : } {i : Fin n} {j : Fin n} (h : i j) :
i j