Daniel
Daniel
What I did for ideals is have the definitions in `ring0`, and then have an abbreviation in `ring_quotient` of `J \ R/I == ring0.ideal(R//I,AI,MI,J)` So, as you suspect, the notation...
I found this in [here](https://isabelle.in.tum.de/doc/isar-ref.pdf): ```code The body consists of context elements: fixes x :: τ (mx) declares a local parameter of type τ and mixfix annotation mx (both are...
I did the `monoid` file, since it was simpler. I added a `sublocale` for a submonoid with an `abbreviation` ```isabelle (* This file is a part of IsarMathLib - a...
I agree with your last point that abbreviation looks better than a definition; but definitions carry over (in an ugly way t `monoid.monoper(x,y)`) and abbreviations do not. What was thinking...
There are no problems referencing results from a parent locale. The problem is proving something is a sublocale. I gave you the example of a subgroup. Since `restrict(P,HxH)` does not...
I have not been looking at this, as I have been sick lately. Sorry. After thinking on it, to carry things over the way you intend to leave it as...
For the 3rd step, we need this [issue](https://github.com/SKolodynski/IsarMathLib/issues/8)
In topgroup, there are some theorems on A\B and \A that are just set theoretic. In my opinion you should provide a proof that anything in group4 is in group0,...
Once you have a locale with notation, the theorems of the other locales specialize. If you read inv_in_group from topgroup, you will see additive notation. No need to prove it...
It looks much better, yes.