equal
deleted
inserted
replaced
15 |
15 |
16 The enterprising reader might consider proving all of Lagrange's |
16 The enterprising reader might consider proving all of Lagrange's |
17 theorem. *} |
17 theorem. *} |
18 |
18 |
19 definition |
19 definition |
20 sq :: "'a::times => 'a" |
20 sq :: "'a::times => 'a" where |
21 "sq x == x*x" |
21 "sq x == x*x" |
22 |
22 |
23 text {* The following lemma essentially shows that every natural |
23 text {* The following lemma essentially shows that every natural |
24 number is the sum of four squares, provided all prime numbers are. |
24 number is the sum of four squares, provided all prime numbers are. |
25 However, this is an abstract theorem about commutative rings. It has, |
25 However, this is an abstract theorem about commutative rings. It has, |