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.