equal
deleted
inserted
replaced
13 \ (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \ |
13 \ (sq x1 + sq x2 + sq x3 + sq x4) * (sq y1 + sq y2 + sq y3 + sq y4) = \ |
14 \ sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + \ |
14 \ sq(x1*y1 - x2*y2 - x3*y3 - x4*y4) + \ |
15 \ sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + \ |
15 \ sq(x1*y2 + x2*y1 + x3*y4 - x4*y3) + \ |
16 \ sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + \ |
16 \ sq(x1*y3 - x2*y4 + x3*y1 + x4*y2) + \ |
17 \ sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"; |
17 \ sq(x1*y4 + x2*y3 - x3*y2 + x4*y1)"; |
18 by(cring_simp 1); |
18 (*Takes up to three minutes...*) |
|
19 by (cring_simp 1); |
19 qed "Lagrange_lemma"; |
20 qed "Lagrange_lemma"; |