mathlib

mathlib copied to clipboard

Multiplicativize the existing add_group_seminorm material.

---

Currently, we have two ways to talk about (additive group) seminorms:

• add_group_seminorm
• seminormed_add_comm_group.core

I want to get rid of the second way and make seminormed groups depend on seminorms (rather than the other way around, as it is today). Now, I am adding multiplicative normed groups in #15705 so I need multiplicative seminorms to make the above plan work, and multiplicativising the API isn't much more work.

You will notice that the above doesn't get us rid of normed_add_comm_group.core. This will get solved once we introduce norms, which I'm planning to do in a separate PR and which I think is desirable anyway to be able to state results such as Asplund's averaging technique.

Build failed (retrying...):

• Build mathlib

Build failed (retrying...):

• Build mathlib

Canceled.

bors d+

:v: YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests