Commit 2023-02-14 08:18 cc5c152a

View on Github →

feat: port Data.Nat.Count (#2209)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Count.lean

added def Nat.CountSet.fintype

added def Nat.count

added theorem Nat.count_add'

added theorem Nat.count_add

added theorem Nat.count_eq_card_filter_range

added theorem Nat.count_eq_card_fintype

added theorem Nat.count_injective

added theorem Nat.count_le_card

added theorem Nat.count_le_cardinal

added theorem Nat.count_lt_card

added theorem Nat.count_lt_count_succ_iff

added theorem Nat.count_mono_left

added theorem Nat.count_monotone

added theorem Nat.count_one

added theorem Nat.count_strict_mono

added theorem Nat.count_succ'

added theorem Nat.count_succ

added theorem Nat.count_succ_eq_count_iff

added theorem Nat.count_succ_eq_succ_count_iff

added theorem Nat.count_zero

added theorem Nat.lt_of_count_lt_count