Theorem Fintype.card_fin_lt_of_le

Modification history

2023-09-02 20:42
Mathlib/Data/Fintype/Card.lean
feat: Elements less than some value of a sorted tuple are at the beginning of the tuple. (#6728) …
Added Fintype.card_fin_lt_of_leView on Github →