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

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

 680theorem radical_prime' {p : ℕ} (hp : Prime p) : radical p = p := by

proof body

Term-mode proof.

 681  have hp' : Nat.Prime p := (prime_iff p).1 hp
 682  simp only [radical]
 683  rw [Nat.Prime.primeFactors hp']
 684  simp
 685
 686/-! ### Totient as cardinality -/
 687
 688/-- φ(n) = |{a ∈ [0,n) : gcd(n,a) = 1}|. -/

depends on (4)

Lean names referenced from this declaration's body.