Commit 2023-12-13 08:05 441b6cef

View on Github →

feat(Combinatorics): definition and basic properties of Schnirelmann density (#7342) Provide the definition of the Schnirelmann density, basic properties of it, and some simple useful calculations.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Schnirelmann.lean

added theorem exists_of_schnirelmannDensity_eq_zero

added theorem le_schnirelmannDensity_iff

added theorem schnirelmannDensity_congr'

added theorem schnirelmannDensity_congr

added theorem schnirelmannDensity_diff_singleton_zero

added theorem schnirelmannDensity_empty

added theorem schnirelmannDensity_eq_one_iff

added theorem schnirelmannDensity_eq_one_iff_of_zero_mem

added theorem schnirelmannDensity_eq_zero_of_one_not_mem

added theorem schnirelmannDensity_finite

added theorem schnirelmannDensity_finset

added theorem schnirelmannDensity_insert_zero

added theorem schnirelmannDensity_le_div

added theorem schnirelmannDensity_le_iff_forall

added theorem schnirelmannDensity_le_of_le

added theorem schnirelmannDensity_le_of_not_mem

added theorem schnirelmannDensity_le_of_subset

added theorem schnirelmannDensity_le_one

added theorem schnirelmannDensity_lt_iff

added theorem schnirelmannDensity_mul_le_card_filter

added theorem schnirelmannDensity_nonneg

added theorem schnirelmannDensity_setOf_Odd

added theorem schnirelmannDensity_setOf_even

added theorem schnirelmannDensity_setOf_mod_eq_one

added theorem schnirelmannDensity_setOf_modeq_one

added theorem schnirelmannDensity_setOf_prime

added theorem schnirelmannDensity_univ

Modified Mathlib/Data/Nat/Order/Basic.lean

added theorem Nat.one_mod_of_ne_one

Modified docs/references.bib