Rings with multiplicative norm

Stream: PR reviews

[David Loeffler]

My now-merged PR 22842 defined a mixin class for normed rings with a strictly multiplicative (not just sub-multiplicative) norm. Following up on this, I have a bunch of PR's which generalise results currently proved for normed fields or normed division rings to this more general context, which should be fairly easy to review.

[David Loeffler]

#23295 : generalize some results about normed rings to seminorms (done, thanks Eric!)

[David Loeffler]

#23348 : define a NormMulClass instance on p-adic integers (depends on 23295)

[David Loeffler]

#23347 : results about IsBigO etc

[David Loeffler]

#23378 : UnitSphere, UnitBall etc

[David Loeffler]

#23376 : multiplication as a Dilation

[Eric Wieser]

Thanks for splitting these into nice small pieces!

[Eric Wieser]

As a follow-up, it would be good to go through the existing instances for docs#NormOneClass and see which types are good candicates for NormMulClass