isabelle/valid/mathd_algebra_509.thy (10 lines of code) (raw):
(*
Authors: Albert Qiaochu Jiang
*)
theory mathd_algebra_509 imports
Complex_Main
begin
theorem mathd_algebra_509:
"sqrt ((5 / sqrt 80 + sqrt 845 / 9 + sqrt 45) / sqrt 5) = 13 / 6"
sorry
end