`arithId_isMultiplicative`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

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

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 369/-- π(5) = 3. -/
 370theorem primeCounting_five : primeCounting 5 = 3 := by
 371  native_decide
 372

papers checked against this theorem

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