Problems because of notation

[dan323]

@SKolodynski I tried to create a subgroup locale and show

group0 H "restrict(P,H\<times>H)"

but it would not work as groper is defined without limitation on the elements you are operating over; hence I cannot show that

x\<cdot>y == restrict(P,H\<times>H)`\<langle>x,y\<rangle>

as x and y need not be elements in H

One thing I thought of is to write the notation as abbreviations right after the locale creation, since they are not really definitions but notations. Another is to define a new operation for each sublocale (I did this for quotients, but that makes more sense since the operation is different)

Of course, this is just a suggestion. :smile: