src/HOL/Number_Theory/Fib.thy
changeset 63167 0909deb8059b
parent 62429 25271ff79171
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Number_Theory/Fib.thy	Thu May 26 16:57:14 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Thu May 26 17:51:22 2016 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  qed
     1.5  
     1.6  lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
     1.7 -    -- \<open>Law 6.111\<close>
     1.8 +    \<comment> \<open>Law 6.111\<close>
     1.9    by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
    1.10  
    1.11  theorem fib_mult_eq_setsum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"