Zulip Chat Archive
Stream: mathlib4
Topic: op_norm tactic
Yury G. Kudryashov (Jun 11 2023 at 00:54):
(deleted)
Yury G. Kudryashov (Jun 11 2023 at 00:54):
(deleted)
Yury G. Kudryashov (Jun 11 2023 at 00:56):
(deleted)
Yury G. Kudryashov (Jun 11 2023 at 00:57):
(deleted)
Yury G. Kudryashov (Jun 11 2023 at 02:13):
There were some false claims in the deleted posts. I'll think about it and possibly start this topic again later.
Last updated: May 02 2025 at 03:31 UTC