Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-13 16:39 2084baf2

View on Github →

feat(set_theory/ordinal/basic): mark type_fintype as simp (#15194) This PR does the following:

  • move type_fintype along with some other lemmas from set_theory/ordinal/arithmetic.lean to set_theory/ordinal/basic.lean.
  • tag type_fintype as simp.
  • untag various lemmas as simp, since they can now be proved by it.

Estimated changes

deleted theorem ordinal.card_eq_nat
deleted theorem ordinal.card_le_nat
deleted theorem ordinal.card_lt_nat
deleted theorem ordinal.nat_le_card
deleted theorem ordinal.nat_lt_card
deleted theorem ordinal.type_fin
deleted theorem ordinal.type_fintype
added theorem ordinal.card_eq_nat
added theorem ordinal.card_le_nat
added theorem ordinal.card_lt_nat
added theorem ordinal.nat_le_card
added theorem ordinal.nat_lt_card
added theorem ordinal.type_fin
added theorem ordinal.type_fintype
modified theorem ordinal.type_pempty
modified theorem ordinal.type_punit
modified theorem ordinal.type_unit