Commit 2025-07-11 20:10 613e6f1c
View on Github →chore(Analysis/InnerProductSpace/Positive): remove additional hypothesis of completeness when it's finite (#27007)
chore(Analysis/InnerProductSpace/Positive): remove additional hypothesis of completeness when it's finite (#27007)