Theorem Fin.ne_of_vne
Modification history
2024-08-14 01:35
Mathlib/Init/Data/Fin/Basic.lean
chore: delete `Init.Data.Fin.Basic` (#15762)
Deleted Fin.ne_of_vneView on Github →2024-03-01 13:29
Mathlib/Init/Data/Fin/Basic.lean
chore(Init/Fin): deprecate `Fin.eq_of_veq` and `Fin.veq_of_eq` (#10626) …
Modified Fin.ne_of_vneView on Github →