Zulip Chat Archive

Stream: condensed mathematics

Topic: strict isomorphism

Adam Topaz (May 20 2021 at 15:16):

If anyone is bored and wants to tackle a trivial but surprisingly annoying sorry, here's one:
https://github.com/leanprover-community/lean-liquid/blob/cfcf86bbbae43b0ac72bdbab54968f9f1960c468/src/prop819.lean#L37

Scott Morrison (May 20 2021 at 23:30):

Just opened it, and see it's done. Indeed annoying. :-)

Adam Topaz (May 20 2021 at 23:56):

Yeah, I just did it :)

Last updated: Dec 20 2023 at 11:08 UTC