`arithId`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 330/-! ### Identity function (for Dirichlet algebra) -/
 331
 332/-- The identity arithmetic function id(n) = n. -/
 333abbrev arithId : ArithmeticFunction ℕ := ArithmeticFunction.id
 334
 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

papers checked against this theorem

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