Zulip Chat Archive

Stream: new members

Topic: Assistance in proof

Suvendu Kar (Jun 22 2023 at 17:06):

Can Someone please say, how to proceed with the following proof of if A,B are Hilbert-Schmidt operator then A+B also?

Martin Dvořák (Jun 22 2023 at 17:09):

If you provide a copy-pastable code (ideally #mwe) rather than a screenshot with code, people will be more likely to help you.

Kevin Buzzard (Jun 22 2023 at 17:10):

Do you know a maths proof?

Notification Bot (Jun 23 2023 at 02:08):

This topic was moved here from #lean4 > Assistance in proof by Scott Morrison.

Scott Morrison (Jun 23 2023 at 02:09):

I've moved this to the new members thread. (Other suggestions?) I think we should try to preserve lean4 for discussion about the language itself, going forward.

Last updated: Dec 20 2023 at 11:08 UTC