Commit 2023-11-13 07:42 6924ba8e

View on Github →

chore: Fix name of Nat.card_mono (#8340) This was accidentally put in the PartENat namespace in #8202. Also add Set.Infinite.card_eq_zero and fix capitalisation errors.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Finite.lean

added theorem Nat.card_mono

deleted theorem PartENat.card_mono

deleted theorem PartENat.card_pLift

added theorem PartENat.card_plift

deleted theorem PartENat.card_uLift

added theorem PartENat.card_ulift

added theorem Set.Infinite.card_eq_zero