Mathlib v3 is deprecated. Go to Mathlib v4

Theorem fintype.card_coe

Modification history

2022-11-18 03:59
src/data/fintype/basic.lean
refactor(data/fintype/basic): split file (#17578)
Modified fintype.card_coeView on Github →
2022-03-30 03:51
src/data/fintype/basic.lean
fix(data/fintype/basic): generalize fintype instance for fintype.card_coe (#13055)
Modified fintype.card_coeView on Github →
2018-08-14 01:44
data/fintype.lean
feat(set_theory/cardinal): finite lower bound on cardinality
Added fintype.card_coeView on Github →