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

sigma_one_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)

 202theorem sigma_one_prime {p : ℕ} (hp : Prime p) : sigma 1 p = p + 1 := by

proof body

Term-mode proof.

 203  have hp' : Nat.Prime p := (prime_iff p).1 hp
 204  simp only [sigma_one_apply, hp'.divisors]
 205  have h_ne : (1 : ℕ) ≠ p := hp'.one_lt.ne'.symm
 206  rw [Finset.sum_insert (by simp [h_ne]), Finset.sum_singleton, add_comm]
 207
 208/-- σ_k(p) = 1 + p^k for prime p. -/

depends on (8)

Lean names referenced from this declaration's body.