Splitting `OperatorNorm.lean`

Stream: mathlib4

[David Loeffler]

I had some lemmas I wanted to add to Analysis/NormedSpace/OperatorNorm.lean, and I got so fed up with trying to understand the layout of that file (a 2300-line overgrown tangled mess) that I found myself splitting it up into 8 smaller files.

I've posted a PR for the split at #10990 – there are no changes to the code, just moving stuff around. I'd be very grateful for a quick review of this PR if possible, since large-file-split PRs are liable to bit-rot very quickly.

[Ruben Van de Velde]

Is " feat(Analysis/NormedSpace): operator norm of fst / snd projn" supposed to be in there?

[Johan Commelin]

8 smaller files, of which the smallest is 600 lines.

Do you mean s/smallest/largest/?

[Ruben Van de Velde]

Ruben Van de Velde said:

Is " feat(Analysis/NormedSpace): operator norm of fst / snd projn" supposed to be in there?

Oh, I didn't read the PR summary

[David Loeffler]

Ruben Van de Velde said:

Is " feat(Analysis/NormedSpace): operator norm of fst / snd projn" supposed to be in there?

It isn't there. I reverted those changes in a later commit but the commit message is still there.

[David Loeffler]

Ruben Van de Velde said:

Oh, I didn't read the PR summary

No, I just added that remark after your message :-)

[David Loeffler]

Johan Commelin said:

8 smaller files, of which the smallest is 600 lines.

Do you mean s/smallest/largest/?

8 x 600 > 2300 :smile:

[Patrick Massot]

And people say that modern number theorists can’t do actual numbers…

[David Loeffler]

Thanks Ruben and Johan for the super-quick responses!