vonMangoldt_nonneg

Mathlib.NumberTheory.VonMangoldt

URI: https://scilib.ai/kg/mathlib#ArithmeticFunction.vonMangoldt_nonneg

← MathLib Explorer

English

Λ(n) ≥ 0 for all n ∈ ℕ.

Русский

Λ(n) неотрицательно для всех n ∈ ℕ.

LaTeX

$$$$0 \le \Lambda(n) \quad \text{for all } n \in \mathbb{N}.$$$$

Lean4

@[simp]
theorem vonMangoldt_nonneg {n : ℕ} : 0 ≤ Λ n := by
  rw [vonMangoldt_apply]
  split_ifs
  · exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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