[Merged by Bors] - chore(Analysis/InnerProductSpace/MulOpposite): `NormedAddCommGroup` -> `SeminormedAddCommGroup`#30695

themathqueen wants to merge 10 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

themathqueen:inner_op_chorethemathqueen/mathlib4:inner_op_choreCopy head branch name to clipboard