Theorem Nat.count_of_forall_not

Modification history

2024-10-28 00:34

Mathlib/Data/Nat/Count.lean

feat: some trivialities about Nat.primeCounting and Finset.card/count (#17037) …

Deleted Nat.count_of_forall_not View on Github →

2024-06-12 08:11

Mathlib/Data/Nat/Count.lean

feat: `@[simp]` `Nat.count` / `Nat.nth` of `fun _ ↦ True`, `False` (#13378)

Added Nat.count_of_forall_not View on Github →