Zulip Chat Archive

Stream: new members

Topic: RFC: operator norm

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Jan-David Salchow (Dec 29 2018 at 09:59):

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

view this post on Zulip Chris Hughes (Dec 29 2018 at 10:02):

put it inside a section

Last updated: May 11 2021 at 21:10 UTC