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.

Estimated changes