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