Theorem Fin.vne_of_ne

Modification history

2024-08-14 01:35
Mathlib/Init/Data/Fin/Basic.lean
chore: delete `Init.Data.Fin.Basic` (#15762)
Deleted Fin.vne_of_neView 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.vne_of_neView on Github →
2022-11-22 07:59
Mathlib/Init/Data/Fin/Basic.lean
feat: add `fun x ↦ t` syntax (#617)
Modified Fin.vne_of_neView on Github →
2022-11-03 02:45
Mathlib/Init/Data/Fin/Basic.lean
feat: port Logic.Unique (#512)
Added Fin.vne_of_neView on Github →