author | nipkow |
Fri, 29 Nov 1996 15:11:37 +0100 | |
changeset 2281 | e00c13a29eda |
child 3018 | e65b60b28341 |
permissions | -rw-r--r-- |
(* Title: HOL/Integ/IntRing.ML ID: $Id$ Author: Tobias Nipkow and Markus Wenzel Copyright 1996 TU Muenchen The instantiation of Lagrange's lemma for int. *) open IntRing; goal thy "!!i1::int. \ \ (sq i1 + sq i2 + sq i3 + sq i4) * (sq j1 + sq j2 + sq j3 + sq j4) = \ \ sq(i1*j1 - i2*j2 - i3*j3 - i4*j4) + \ \ sq(i1*j2 + i2*j1 + i3*j4 - i4*j3) + \ \ sq(i1*j3 - i2*j4 + i3*j1 + i4*j2) + \ \ sq(i1*j4 + i2*j3 - i3*j2 + i4*j1)"; br Lagrange_lemma 1; qed "Lagrange_lemma_int";