Commit 2024-09-25 20:50 691fdda9
View on Github →chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup (#17007)
replace the assumption NormedAddCommGroup to SemiNormedAddCommGroup in various places.
motivation: with the weakened assumption the results apply to InnerProductSpace without definite assumption.
This is suggested in #16707, and continues from #14024.