theorem
proved
term proof
radical_thirty
show as:
view Lean formalization →
formal statement (Lean)
835theorem radical_thirty : radical 30 = 30 := by native_decide
proof body
Term-mode proof.
836
837/-- rad(60) = 30. -/