Commit 2023-11-10 21:41 52c6af84

View on Github →

feat: When Nat.card is zero (#8202) and lemmas about injectivity/surjectivity of PLift.map/ULift.map.

Estimated changes

modified theorem ULift.map_up
added theorem PLift.map_bijective
added theorem PLift.map_injective
added theorem PLift.map_surjective
added theorem ULift.map_bijective
added theorem ULift.map_injective
added theorem ULift.map_surjective
added theorem Cardinal.toNat_eq_zero
added theorem Cardinal.toNat_ne_zero
added theorem Cardinal.toNat_pos
added theorem Nat.card_eq_zero
added theorem Nat.card_ne_zero
added theorem Nat.card_pos
added theorem Nat.card_pos_iff
modified theorem Nat.finite_of_card_ne_zero
added theorem PartENat.card_mono