## Stream: new members

### Topic: RFC: operator norm

#### Jan-David Salchow (Dec 28 2018 at 22:36):

I've been playing with the space of bounded linear maps between normed space, see https://github.com/jdsalchow/mathlib/blob/calculus/analysis/functional/operator_norm.lean

Before splitting this up into smaller pieces and creating a PR, I thought I better ask for comments. So, comments anybody?

#### Kevin Buzzard (Dec 28 2018 at 23:52):

local attribute[instance] classical.prop_decidable -- people often go for local attribute [instance, priority 0] classical.prop_decidable nowadays because it is less likely to break proofs that actually rely on decidability. This might well not be an issue in this code though.

#### Jan-David Salchow (Dec 29 2018 at 09:59):

Is there a way to forget a local attribute when it's not needed anymore?

#### Chris Hughes (Dec 29 2018 at 10:02):

put it inside a section

Last updated: May 11 2021 at 21:10 UTC