Commit 2025-03-15 00:24 bae52868

View on Github →

feat: move Nat.count_le_cardinal, add variants (#22938)

Estimated changes

Modified Archive/Imo/Imo2024Q3.lean

Modified Mathlib.lean

Modified Mathlib/Data/Nat/Count.lean

deleted theorem Nat.count_le_cardinal

Modified Mathlib/Data/Nat/Nth.lean

Created Mathlib/SetTheory/Cardinal/NatCount.lean

added theorem Nat.count_le_cardinal

added theorem Nat.count_le_setENCard

added theorem Nat.count_le_setNCard