[Merged by Bors] - chore(Analysis/InnerProductSpace): weaken assumptions to SeminormedAddCommGroup

[yoh-tanimoto]

replace the assumption NormedAddCommGroup to SemiNormedAddCommGroup in various places.

motivation: with the weakened assumption the results apply to InnerProductSpace without definite assumption.

This is suggested in #16707, and continues from #14024.

---

I think it should be possible to do the same with IsSymmetric.restrictScalars but CompatibleSMul E E ℝ 𝕜 cannot be synthesized. Can anyone help?

Are there other things that work with SemiNormedAddCommGroup?

I noticed that in InnerProductSpace.Basic there are two instances of InnerProductSpace ℝ ℂ. Should I remove the latter?

[github-actions]

PR summary 0f88afc31f

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 94fe59e.
There were no significant changes against commit 831db37.

[eric-wieser]

I span off #17011 from this; I think that in turn will make some sections more generalizable.

[eric-wieser]

I've done a much more thorough version of this in #17059, but they can be merged in either order.

[eric-wieser]

this is suggested in #16707. I think it should be possible to do the same with IsSymmetric.restrictScalars but CompatibleSMul E E ℝ 𝕜 cannot be synthesized. Can anyone help?

I managed to solve this for you with a letI.

[eric-wieser]

This now looks good to me; I think there are probably more generalizations possible elsewhere, but this already hits quite a lot of them!

Were there any more you wanted help with, or can the help-wanted label go?

[yoh-tanimoto]

Yes, I only checked Basic, Symmetric and Dual. I will see whether more generalizations are possible in other files when I will use them. Thank you very much for your help!

Could you please tell me why #synth CompatibleSMul E E ℝ 𝕜 cannot be synthesized, yet the previous code worked with NormedAddCommGroup?

[j-loreaux]

@yoh-tanimoto I think Eric already explained this above. The issue is that the instance it was trying to use required T2Space, which doesn't hold in seminormed spaces, only normed ones. So it needed explicit help.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style

[eric-wieser]

@yoh-tanimoto I think Eric already explained this above. The issue is that the instance it was trying to use required T2Space, which doesn't hold in seminormed spaces, only normed ones. So it needed explicit help.

Actually the issue here was more subtle; the lemma was about a non-instance typeclass argument provided through a messy @ _ _ _ invocation. I switched this to use letI for clarify, but you would need the same letI in the #synth for it to work.

[yoh-tanimoto]

Yes, I meant that. Even with NormedAddCommGroup, I got #synth error (as in my question above).