RFC: operator norm

Stream: new members

[Jan-David Salchow]

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]

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]

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

[Chris Hughes]

put it inside a section