Thu, 17 May 2007 19:29:39 +0200 | huffman | add classes ring_no_zero_divisors and dom | changeset | files |
Thu, 17 May 2007 19:12:47 +0200 | huffman | generalize class restrictions on some lemmas | changeset | files |
Thu, 17 May 2007 18:32:17 +0200 | huffman | added classes ring_no_zero_divisors and dom (non-commutative version of idom); | changeset | files |
Thu, 17 May 2007 13:37:24 +0200 | paulson | Added three items to the signature | changeset | files |
Thu, 17 May 2007 08:53:57 +0200 | huffman | generalize some lemmas from field to division_ring | changeset | files |
Thu, 17 May 2007 08:42:51 +0200 | huffman | instance division_ring < no_zero_divisors; clean up field instance proofs | changeset | files |