Commit 2024-10-04 23:30 11fa9c00
View on Github →chore(Analysis/InnerProductSpace/Dual): weaken assumptions to SeminormedAddCommGroup (#17416)
Replace the NormedAddCommGroup assumption with SemiNormedAddCommGroup where possible.
motivation: we need toDual, toDualMap etc. to define an InnerProductSpace instance for SeparationQuotient.
suggested in #16707.