pith. machine review for the scientific record. sign in
theorem proved term proof

bigOmega_prime

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

 458theorem bigOmega_prime {p : ℕ} (hp : Prime p) : bigOmega p = 1 := by

proof body

Term-mode proof.

 459  have hp' : Nat.Prime p := (prime_iff p).1 hp
 460  exact ArithmeticFunction.cardFactors_apply_prime hp'
 461
 462/-! ### Additional totient values -/
 463
 464/-- φ(2) = 1. -/

depends on (4)

Lean names referenced from this declaration's body.