The file 'group.v' as Latin-1 characters

  1  V  a  r  i  a  b  l  e  ␣  G  ␣  :  ␣  S  e  t  . EOL(␊)
  2  V  a  r  i  a  b  l  e  ␣  o  p  e  r  a  t  i  o  n  ␣  :  ␣  G  ␣  -  >  ␣  G  ␣  -  >  ␣  G  . EOL(␊)
  3  V  a  r  i  a  b  l  e  ␣  e  ␣  :  ␣  G  . EOL(␊)
  4  V  a  r  i  a  b  l  e  ␣  i  n  v  ␣  :  ␣  G  ␣  -  >  ␣  G  . EOL(␊)
  5 EOL(␊)
  6  I  n  f  i  x  ␣  "  ×  "  ␣  :  =  ␣  o  p  e  r  a  t  i  o  n  ␣  (  a  t  ␣  l  e  v  e  l  ␣  5  0  ,  ␣  l  e  f  t  ␣  a  s  s  o  c  i  a  t  i  v  i  t  y  )  . EOL(␊)
  7 EOL(␊)
  8  H  y  p  o  t  h  e  s  i  s  ␣  a  s  s  o  c  i  a  t  i  v  i  t  y  ␣  :  ␣  f  o  r  a  l  l  ␣  x  ␣  y  ␣  z  ␣  :  ␣  G  ,  ␣  (  x  ␣  ×  ␣  y  )  ␣  ×  ␣  z  ␣  =  ␣  x  ␣  ×  ␣  (  y  ␣  ×  ␣  z  )  . EOL(␊)
  9  H  y  p  o  t  h  e  s  i  s  ␣  i  d  e  n  t  i  t  y  ␣  :  ␣  f  o  r  a  l  l  ␣  x  ␣  :  ␣  G  ,  ␣  (  x  ␣  ×  ␣  e  )  ␣  =  ␣  e  ␣  /  \  ␣  e  ␣  ×  ␣  x  ␣  =  ␣  x  . EOL(␊)
 10  H  y  p  o  t  h  e  s  i  s  ␣  i  n  v  e  r  s  e  ␣  :  ␣  f  o  r  a  l  l  ␣  x  ␣  :  ␣  G  ,  ␣  (  x  ␣  ×  ␣  i  n  v  ␣  x  )  ␣  =  ␣  e  ␣  /  \  ␣  i  n  v  ␣  x  ␣  ×  ␣  x  ␣  =  ␣  x  . EOL(␊)
 11 EOL(␊)
 12  T  h  e  o  r  e  m  ␣  l  a  t  i  n  _  s  q  u  a  r  e  _  p  r  o  p  e  r  t  y  ␣  :  ␣  f  o  r  a  l  l  ␣  a  ␣  b  ␣  :  ␣  G  ,  ␣  e  x  i  s  t  s  ␣  x  ␣  :  ␣  G  ,  ␣  a  ␣  ×  ␣  x  ␣  =  ␣  b  . EOL(␊)
 13  ␣  ␣  i  n  t  r  o  s  ␣  a  ␣  b  . EOL(␊)
 14  ␣  ␣  e  x  i  s  t  s  ␣  (  i  n  v  ␣  a  ␣  ×  ␣  b  )  . EOL(␊)
 15  ␣  ␣  r  e  w  r  i  t  e  ␣  <  -  ␣  a  s  s  o  c  i  a  t  i  v  i  t  y  . EOL(␊)
 16  ␣  ␣  d  e  s  t  r  u  c  t  ␣  i  n  v  e  r  s  e  ␣  w  i  t  h  ␣  (  x  :  =  a  )  ␣  a  s  ␣  [  H  ␣  _  ]  . EOL(␊)
 17  ␣  ␣  r  e  w  r  i  t  e  ␣  H  . EOL(␊)
 18  ␣  ␣  d  e  s  t  r  u  c  t  ␣  i  d  e  n  t  i  t  y  ␣  w  i  t  h  ␣  (  x  :  =  b  )  ␣  a  s  ␣  [  _  ␣  H  '  ]  . EOL(␊)
 19  ␣  ␣  t  r  i  v  i  a  l  . EOL(␊)
 20  Q  e  d  . EOL(␊)