!4#3708 Analysis.NormedSpace.OperatorNorm

Stream: mathlib4

[Jeremy Tan]

This thread is for !4#3708, which I believe is the most important file to work on right now besides LinearAlgebra.Determinant

[Jeremy Tan]

I have a stash with my own initial fixes. @Anatole Dedecker can I push this first before everyone else works on this?

[Jeremy Tan]

(warning: literally tons of etas are in my stash)

[Anatole Dedecker]

I just opened the pull request with the autogenerated output, you can push all you want right now

[Jeremy Tan]

I pushed there, now this great community can come and fix the remaining errors/speed up compilation somewhat

[Jeremy Tan]

@Anatole Dedecker did you have any stuff to push before me?

[Jeremy Tan]

Now there is a name clash between ContinuousLinearMap.mul here and an identically named declaration in Topology.Algebra.Module.Basic. The latter was nameless in mathlib3 – should I make the TAMB declaration nameless again?

[Mario Carneiro]

the lean 4 naming convention for instances starts with inst, not sure where exactly we landed on that

[Mario Carneiro]

this looks more like a translated lean 3 name

[Jeremy Tan]

So should I change TAMB's mul to instMul?

[Jeremy Tan]

(I have went ahead with this in the PR, alongside naming a few instances in the dependency)

[Eric Wieser]

Mario Carneiro said:

the lean 4 naming convention for instances starts with inst, not sure where exactly we landed on that

I also remember a thread settling on this. But in practice I think all our instances still have the wrong names.

[Anatole Dedecker]

Jeremy Tan said:

Anatole Dedecker did you have any stuff to push before me?

No I don’t, I was distracted by trying to understand why we need all these etas in the first place

[Eric Wieser]

I have a paper about why they're needed which was sent to CICM

[Anatole Dedecker]

Oh I would love to read it

[Johan Commelin]

I fixed error around L406. But this file is really slow... Very painful to work on.