Commit 2024-10-28 00:34 91530d46

View on Github →

feat: some trivialities about Nat.primeCounting and Finset.card/count (#17037) Also move some general results out of PrimeCounting.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.card_filter_eq_iff

added theorem Finset.card_filter_eq_zero_iff

added theorem Finset.eq_iff_card_ge_of_superset

added theorem Finset.eq_iff_card_le_of_subset

deleted theorem Finset.filter_card_eq

Modified Mathlib/Data/Nat/Count.lean

added theorem Nat.count_iff_forall

added theorem Nat.count_iff_forall_not

added theorem Nat.count_le

deleted theorem Nat.count_of_forall

deleted theorem Nat.count_of_forall_not

Modified Mathlib/Data/Nat/Nth.lean

Created Mathlib/Data/Nat/Prime/Nth.lean

added theorem Nat.nth_prime_one_eq_three

added theorem Nat.nth_prime_zero_eq_two

Modified Mathlib/NumberTheory/PrimeCounting.lean

added theorem Nat.primeCounting'_eq_zero_iff

added theorem Nat.primeCounting_eq_zero_iff

added theorem Nat.primeCounting_one

added theorem Nat.primeCounting_zero

deleted theorem Nat.zeroth_prime_eq_two