Resolved: The renaming and synonymizing has been done. Proposal: Rename the inner-product-spaces to inner-products. Create the tag synonym inner-product-spaces $\to$ inner-products. Create the tag synonym dot-product $\to$ inner-products. Create the tag synonym scalar-product $\to$ inner-produ...