Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-08 16:03 1519cd77

View on Github →

chore(set_theory/cardinal): more simp, fix LHS/RHS (#10212) While coe (fintype.card α) is a larger expression than #α, it allows us to compute the cardinality of a finite type provided that we have a simp lemma for fintype.card α. It also plays well with lemmas about coercions from nat and cardinal.lift.

  • rename cardinal.fintype_card to cardinal.mk_fintype, make it a @[simp] lemma;
  • deduce other cases (bool, Prop, unique, is_empty) from it;
  • rename cardinal.finset_card to cardinal.mk_finset, swap LHS/RHS;
  • rename ordinal.fintype_card to ordinal.type_fintype.

Estimated changes

added theorem fintype.card_Prop
modified theorem is_noetherian.dim_lt_omega
deleted theorem cardinal.finset_card
deleted theorem cardinal.fintype_card
modified theorem cardinal.mk_Prop
modified theorem cardinal.mk_bool
modified theorem cardinal.mk_eq_one
modified theorem cardinal.mk_eq_zero
modified theorem cardinal.mk_fin
added theorem cardinal.mk_finset
added theorem cardinal.mk_fintype
modified theorem cardinal.mk_to_nat_eq_card
deleted theorem ordinal.fintype_card
added theorem ordinal.type_fintype