isabelle/valid/mathd_algebra_22.thy (10 lines of code) (raw):

(* Authors: Albert Qiaochu Jiang *) theory mathd_algebra_22 imports Complex_Main begin theorem mathd_algebra_22: "(log 2 (5^4)) / (log 2 (5^2)) = 2" sorry end