Theorem Fin.coe_int_sub_eq_ite

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) …
Added Fin.coe_int_sub_eq_iteView on Github →