Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fintype.card_subtype_or_disjoint

Modification history

2022-11-18 03:59
src/data/fintype/basic.lean
refactor(data/fintype/basic): split file (#17578)
Modified fintype.card_subtype_or_disjointView on Github →
2021-08-16 16:19
src/data/fintype/basic.lean
feat(data/fintype/basic): card_sum, card_subtype_or (#8490)
Added fintype.card_subtype_or_disjointView on Github →