Theorem Fin.eq_one_of_neq_zero

Modification history

2024-09-29 17:58

Mathlib/Data/Fin/Basic.lean

feat: `fin_omega`, a wrapper around `omega` to help with `Fin` arithmetic goals. (#16651) …

Modified Fin.eq_one_of_neq_zero View on Github →

2023-11-01 06:34

Mathlib/Data/Fin/Basic.lean

feat(CategoryTheory): the category of composable arrows (#7999)

Added Fin.eq_one_of_neq_zero View on Github →