residueClass_le

Mathlib.NumberTheory.LSeries.PrimesInAP

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.vonMangoldt.residueClass_le

English

The residueClass evaluated at 0 is zero: residueClass a 0 = 0.

Русский

Значение residueClass в 0 равно нулю: residueClass a 0 = 0.

LaTeX

$$residueClass a 0 = 0$$

Lean4

theorem residueClass_le (n : ℕ) : residueClass a n ≤ vonMangoldt n :=
  Set.indicator_apply_le' (fun _ ↦ le_rfl) (fun _ ↦ vonMangoldt_nonneg)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru