`arithId_apply`

proved

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions
domain: NumberTheory
line: 338 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 338.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 335@[simp] theorem arithId_def : arithId = ArithmeticFunction.id := rfl
 336
 337/-- id(n) = n. -/
 338theorem arithId_apply {n : ℕ} : arithId n = n := by
 339  simp [arithId]
 340
 341/-- The identity function is multiplicative. -/
 342theorem arithId_isMultiplicative : ArithmeticFunction.IsMultiplicative arithId := by
 343  simp only [arithId]
 344  exact ArithmeticFunction.isMultiplicative_id
 345
 346/-! ### Prime counting function π -/
 347
 348/-- The prime counting function π(n) = #{p ≤ n : p prime}. -/
 349def primeCounting (n : ℕ) : ℕ := Nat.primeCounting n
 350
 351@[simp] theorem primeCounting_def {n : ℕ} : primeCounting n = Nat.primeCounting n := rfl
 352
 353/-- π(0) = 0. -/
 354theorem primeCounting_zero : primeCounting 0 = 0 := by
 355  simp [primeCounting]
 356
 357/-- π(1) = 0. -/
 358theorem primeCounting_one : primeCounting 1 = 0 := by
 359  simp [primeCounting, Nat.primeCounting]
 360
 361/-- π(2) = 1. -/
 362theorem primeCounting_two : primeCounting 2 = 1 := by
 363  native_decide
 364
 365/-- π(3) = 2. -/
 366theorem primeCounting_three : primeCounting 3 = 2 := by
 367  native_decide
 368

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.