7.1. AddGroup versus AddMonoid🔗

It's not clear if at some point there will be need to work with additive groups. There is one place where they seem necessary:

1. If we want to put a topology (or more broadly, an uniform structure) induced by the quasinorm, we would need to use the distance d(x,y) = ‖x - y‖. However, this may not be necessary for the main results, and it may be assumed only in the constructor for the topology. In such cases, it is important to have the extra assumption that ‖-x‖ = ‖x‖ to define the uniformity.

In case we require an AddGroup for the EQuasinorm definition, we will also need an ESeminormedAddGroup class for stating the results in ELorentz, because they depend on the class ESeminormedAddMonoid.

7.2. Verso-blueprint🔗

verso-blueprint is developed using LLMs and despite working well in some aspects, does not as I would like in others. The web style of its components is not very formal and it does not emit proper \LaTeX for the theorems and similar constructs. I chose to make some patches to its style in the module Blueprint.StylePatches, and I used an LLM to fight those issues introduced by some LLM. I don't know if those patches introduce other problems.

Despite that, it seemed to be the easiest option to integrate with the project and it has the benefit of being written in Lean, so hacking it is easier for me than the alternatives.

Some feature requests:

• Add a place to write informal proofs or informal comments about the proofs other than the theorem statements.

• Add a details spoiler in definitions and proofs showing the bodies of the declarations (preferably with the Verso hovers 🙂).