5 theory Commutative_Ring_Ex |
5 theory Commutative_Ring_Ex |
6 imports "../Commutative_Ring" |
6 imports "../Commutative_Ring" |
7 begin |
7 begin |
8 |
8 |
9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
9 lemma "4*(x::int)^5*y^3*x^2*3 + x*z + 3^5 = 12*x^7*y^3 + z*x + 243" |
10 by comm_ring |
10 by comm_ring |
11 |
11 |
12 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" |
12 lemma "((x::int) + y)^2 = x^2 + y^2 + 2*x*y" |
13 by comm_ring |
13 by comm_ring |
14 |
14 |
15 lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" |
15 lemma "((x::int) + y)^3 = x^3 + y^3 + 3*x^2*y + 3*y^2*x" |
16 by comm_ring |
16 by comm_ring |
17 |
17 |
18 lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" |
18 lemma "((x::int) - y)^3 = x^3 + 3*x*y^2 + (-3)*y*x^2 - y^3" |
19 by comm_ring |
19 by comm_ring |
20 |
20 |
21 lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" |
21 lemma "((x::int) - y)^2 = x^2 + y^2 - 2*x*y" |
22 by comm_ring |
22 by comm_ring |
23 |
23 |
24 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" |
24 lemma " ((a::int) + b + c)^2 = a^2 + b^2 + c^2 + 2*a*b + 2*b*c + 2*a*c" |
25 by comm_ring |
25 by comm_ring |
26 |
26 |
27 lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c" |
27 lemma "((a::int) - b - c)^2 = a^2 + b^2 + c^2 - 2*a*b + 2*b*c - 2*a*c" |
28 by comm_ring |
28 by comm_ring |
29 |
29 |
30 lemma "(a::int)*b + a*c = a*(b+c)" |
30 lemma "(a::int)*b + a*c = a*(b+c)" |
31 by comm_ring |
31 by comm_ring |
32 |
32 |
33 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" |
33 lemma "(a::int)^2 - b^2 = (a - b) * (a + b)" |
34 by comm_ring |
34 by comm_ring |
35 |
35 |
36 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" |
36 lemma "(a::int)^3 - b^3 = (a - b) * (a^2 + a*b + b^2)" |
37 by comm_ring |
37 by comm_ring |
38 |
38 |
39 lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)" |
39 lemma "(a::int)^3 + b^3 = (a + b) * (a^2 - a*b + b^2)" |
40 by comm_ring |
40 by comm_ring |
41 |
41 |
42 lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" |
42 lemma "(a::int)^4 - b^4 = (a - b) * (a + b)*(a^2 + b^2)" |
43 by comm_ring |
43 by comm_ring |
44 |
44 |
45 lemma "(a::int)^10 - b^10 = (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9 )" |
45 lemma "(a::int)^10 - b^10 = |
46 by comm_ring |
46 (a - b) * (a^9 + a^8*b + a^7*b^2 + a^6*b^3 + a^5*b^4 + a^4*b^5 + a^3*b^6 + a^2*b^7 + a*b^8 + b^9)" |
|
47 by comm_ring |
47 |
48 |
48 end |
49 end |