changeset 69064 | 5840724b1d71 |
parent 67613 | ce654b0e6d69 |
child 69597 | ff784d5a5bfb |
69045:8c240fdeffcb | 69064:5840724b1d71 |
---|---|
736 |
736 |
737 end |
737 end |
738 |
738 |
739 |
739 |
740 locale Dgrp = Dmonoid + |
740 locale Dgrp = Dmonoid + |
741 assumes unit [intro, simp]: "Dmonoid.unit (( ** )) one x" |
741 assumes unit [intro, simp]: "Dmonoid.unit ((**)) one x" |
742 |
742 |
743 begin |
743 begin |
744 |
744 |
745 lemma l_inv_ex [simp]: |
745 lemma l_inv_ex [simp]: |
746 "\<exists>y. y ** x = one" |
746 "\<exists>y. y ** x = one" |