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

radical_le

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)

 849theorem radical_le {n : ℕ} (hn : n ≠ 0) : radical n ≤ n := by

proof body

Term-mode proof.

 850  simp only [radical]
 851  have h := Nat.prod_primeFactors_dvd n
 852  exact Nat.le_of_dvd (Nat.pos_of_ne_zero hn) h
 853
 854/-- rad(1) = 1 (using the general definition). -/

depends on (1)

Lean names referenced from this declaration's body.