Mathlib Map

Theorems · Definition · combinatorics

FinEnum.card

(α : Sort u_1) → [self : FinEnum α] → ℕ

FinEnum.card is the cardinality of the FinEnum

Defined in
Mathlib.Data.FinEnum
Cited by
32 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
FinEnum
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

FinEnum.equiv · cited by 9FinEnum.equivFinEnum.toList · cited by 4FinEnum.toListFinEnum.card_eq_fintypeCard · cited by 4FinEnum.card_eq_fintypeCa…FinEnum.insertNone · cited by 3FinEnum.insertNoneFinEnum.recEmptyOption · cited by 3FinEnum.recEmptyOptionFinEnum.recEmptyOption.eq_def · cited by 2recEmptyOption.eq_defFinEnum.mem_toList · cited by 1FinEnum.mem_toListFinEnum.card_eq_zero · cited by 1FinEnum.card_eq_zeroFinEnum.card_eq_zero_iff · cited by 1FinEnum.card_eq_zero_iffFinEnum.card_fin · cited by 1FinEnum.card_finFinEnum.card_pos · cited by 1FinEnum.card_posFinEnum.card_pos_iff · cited by 1FinEnum.card_pos_iffFinEnum.equiv_down · cited by 0FinEnum.equiv_downFinEnum.equiv_up · cited by 0FinEnum.equiv_upFinEnum.nodup_toList · cited by 0FinEnum.nodup_toListFinEnum · cited by 21FinEnumFinEnum.cardCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • FinEnumstatement and proof · cited by 21

Cited by38

Results whose statement or proof uses this declaration.