[Merged by Bors] - chore(Analysis/InnerProductSpace): remove misleading comment#42123

felixpernegger wants to merge 1 commit into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

felixpernegger:adjointnoncomputablefelixpernegger/mathlib4:adjointnoncomputableCopy head branch name to clipboard