Commit 2025-05-03 01:57 3a8fa588

chore(Analysis/InnerProductSpace): make 𝕜 an explicit argument of inner (#24499) There are two reasons why 𝕜 should be an explicit argument.

• This change makes it so that notations ⟪x, y⟫ and ⟪x, y⟫_𝕜 elaborate properly, so that this notation can be seen in the infoview.
• This change makes is so that the expected type is known whenever using inner. Thus, this PR also removes some now unneccessary type annotations. The argument explicitness now matches that of innerₛₗ and innerSL. notation3 has been replaced by notation, since we don't need the more fancy notation3 elborator.