NormedSpace, BoundedSMul

Stream: mathlib4

[Yury G. Kudryashov]

Recently, @Eric Wieser generalized many theorems from [NormedField K] [NormedSpace K E] to [*NormedRing R] [NormedAddCommGroup E] [Module R E] [BoundedSMul R E]. While the latter spelling is more flexible (e.g., it allows using *SMul classes instead of Module), it is longer and a less readable, at least for a new user. What should we do?

• continue migration to BoundedSMul?
• relax TC assumptions on K in NormedSpace K E to NormedRing and use [NormedSpace K E] (or rename it to NormedModule K E)?

[Yury G. Kudryashov]

Eric, are there situations when we should care about BoundedSMul R E without Module R E assumption?

[Eric Wieser]

In practice right now, probably not; but in future, we might want it for DistribMulAction G E, for instance with G := Units R

[Yury G. Kudryashov]

Note that [BoundedSMul R E] needs [Zero R] and [Zero E]

[Eric Wieser]

Then docs#NonUnitalSeminormedRing.to_boundedSMul is the answer I should have given

[Yury G. Kudryashov]

What do you think about a mixed approach?

• Allow SeminormedRing in NormedSpace, still assume norm_smul_le;
• Assume [NormedSpace R M] instead of [Module R M] [BoundedSMul R M];
• Use BoundedSMul if a lemma works for a typeclass weaker than Module?

[Eric Wieser]

Originally, I had intended to refactor NormedSpace K V to a be a K-bimodule, along the same lines as #7152 (in fact, I did this already in Lean3 but it never landed)

[Eric Wieser]

So my preference would be to leave NormedSpace alone for now, to avoid that refactor becoming harder

[Yury G. Kudryashov]

I see, thanks for the explanation.

[Yury G. Kudryashov]

Then I'll review your Asymptotics PR today.

[Eric Wieser]

#10519 adds another generalization in this direction