schnirelmannDensity_setOf_modeq_one

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 \\neq 1, \\operatorname{schnirelmannDensity}({n \\mid n \\equiv 1 [MOD m]}) = m^{-1}$$

Lean4

theorem schnirelmannDensity_setOf_modeq_one {m : ℕ} : schnirelmannDensity {n | n ≡ 1 [MOD m]} = (m⁻¹ : ℝ) :=
  by
  rcases eq_or_ne m 1 with rfl | hm
  · simp [Nat.modEq_one]
  rw [← schnirelmannDensity_setOf_mod_eq_one hm]
  apply schnirelmannDensity_congr
  ext n
  simp only [Set.mem_setOf_eq, Nat.ModEq, Nat.one_mod_eq_one.mpr hm]

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