Theorem Fin.ne_zero_of_lt

Modification history

2024-05-30 11:57
Mathlib/Data/Fin/Basic.lean
chore: Delete `Data.Fin.OrderHom` (#13147) …
Added Fin.ne_zero_of_ltView on Github →