pith. machine review for the scientific record. sign in
def definition def or abbrev

phiRungPrime

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

Last generation error: Invalid control character at: line 3 column 95 (char 481)

generate prose now

formal statement (Lean)

  62def phiRungPrime (p : ℕ) : ℤ :=

proof body

Definition body.

  63  Int.floor (Real.log (p : ℝ) / Real.log phi)
  64
  65/-- The phi-rung extended completely additively to all positive integers.
  66
  67    For `n ≥ 1`, this is `Σ_p v_p(n) · phiRungPrime(p)`, where `v_p`
  68    is the `p`-adic valuation. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.