Commit 2024-10-16 05:50 a5bdd272

View on Github →

chore: deprecate Fin.ofNat'' (#17759) Now that NeZero is in Lean, Fin.ofNat' already means the right thing.

Estimated changes

deleted theorem Fin.ofNat''_eq_cast
added theorem Fin.ofNat'_eq_cast
deleted theorem Fin.ofNat'_one
deleted theorem Fin.ofNat'_zero