Commit 2026-01-24 18:35 a11a7dd9
View on Github →feat(Data/Fintype/Fin): count elements of Fin n below a natural bound (#34352)
A simple lemma for counting elements of Fin n. Note that we can't immediately reuse things like Finset.Iio because the upper bound is a Nat and might not live in Fin n (a cases argument would work, but would probably be longer overall)