Defining new structures without new fields?

Stream: general

[Ryan Lahfa]

I'm trying to define a Banach ring in Lean, which is a complete normed ring.

For this, I wanted to define a structure, so I defined:

import analysis.normed_space.basic

variables (R: Type*)
structure banach_ring extends normed_ring R, complete_space R

I have multiple questions:

(a) Is it a good idea?
(b) As I understand now, I will have to to_xxx to get the underlying structure that I want in my definitions, should I re-inline the most important facts in the structure definition?
(c) I want to define the notion of Banach A-algebra afterward which is a Banach algebra B with a bounded morphism A → B, am I following a proper path to achieve this?

(My motivation is to define the set of all bounded real "semivaluations" over A of a Banach ring A, i.e. the spectrum of Berkovich.)

[Ryan Lahfa]

Or maybe I should do something like this:

import analysis.normed_space.basic

variables (R: Type*) [normed_ring R]
structure banach_ring extends complete_space R

?

[Johan Commelin]

I would first develop a bunch of stuff where you just assume [normed_ring R] [complete_space R]. For a Banach algebra, it makes sense to make a new defn, since you need the boundedness assumption on the algebra map.

[Ryan Lahfa]

Alright, thank you for the advice!