Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fintype.card_subtype_le

Modification history

2022-11-18 03:59

src/data/fintype/basic.lean

refactor(data/fintype/basic): split file (#17578)

Modified fintype.card_subtype_le View on Github →

2019-09-03 09:24

src/data/fintype.lean

feat(data/fintype): prove `card (subtype p) ≤ card α` (#1383) …

Added fintype.card_subtype_le View on Github →