NormedAlgebra with ring

Stream: mathlib4

[Daniel Weber]

Is there an equivalent of docs#NormedAlgebra where 𝕜 is a NormedCommRing and not a NormedField?

[Jireh Loreaux]

We have docs#BoundedSMul, but that's about it.

[Eric Wieser]

I think BoundedSMul covers precisely the use case you want

[Jireh Loreaux]

But does it work well with the norm? I'm not sure how much we have generalized.

[Eric Wieser]

I put a fair amount of effort into this style of generalization last year

[Daniel Weber]

I need something like docs#norm_smul, but without α being a division ring. More generally, do we have anything about normed rings which aren't division rings but the norm still is multiplicative?

[Eric Wieser]

Presumably norm_smul_le isn't enough for you?

[Eric Wieser]

(a lot of time there is an easy proof using norm_smul, and a slightly more fiddly one using norm_smul_le)

[Eric Wieser]

I think the answer to your question is "no", but I also think there is some past discussion on the matter elsewhere on Zulip, which I'll link if I can find

[Daniel Weber]

I want to generalize #16597, I don't see how to do that with norm_smul_le

[Kevin Buzzard]

How about using docs#Valuation ? Then you can apply the result to the rationals with the usual norm, or with the p-adic norm.

[Daniel Weber]

How does that work? The usual norm doesn't satisfy f (x + y) ≤ max (f x) (f y), unless I'm missing something?

[Kevin Buzzard]

Oh lol yeah good point :-)

[María Inés de Frutos Fernández]

In #15445 I introduce an AlgebraNorm structure and the corresponding AlgebraNormClass:

structure AlgebraNorm (R : Type*) [SeminormedCommRing R] (S : Type*) [Ring S] [Algebra R S] extends
  RingNorm S, Seminorm R S

(I know this is not exactly what you are asking for, but I am pointing it out in case it is helpful.)