# Zulip Chat Archive

## Stream: general

### Topic: Defining new structures without new fields?

#### Ryan Lahfa (Feb 04 2021 at 14:37):

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 (Feb 04 2021 at 14:49):

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 (Feb 04 2021 at 14:57):

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 (Feb 04 2021 at 14:59):

Alright, thank you for the advice!

Last updated: Dec 20 2023 at 11:08 UTC