schnirelmannDensity_setOf_Odd — Mathlib

English

The Schnirelmann density of set {n | n ≡ 1 [MOD m]} equals m^{-1} for m ≠ 1.

Русский

Плотность множества {n | n ≡ 1 [MOD m]} равна m^{-1} при m ≠ 1.

LaTeX

$$\\forall m, m ≠ 1 \\Rightarrow \\operatorname{schnirelmannDensity}( {n \\mid n \\equiv 1 \\ (MOD m)} ) = m^{-1}$$

Lean4

theorem schnirelmannDensity_setOf_Odd : schnirelmannDensity (setOf Odd) = 2⁻¹ :=
  by
  have h : setOf Odd = {n | n % 2 = 1} := Set.ext fun _ => Nat.odd_iff
  simp only [h]
  rw [schnirelmannDensity_setOf_mod_eq_one (by norm_num1), Nat.cast_two]

Похожие утверждения