Zulip Chat Archive
Stream: condensed mathematics
Topic: congr' 5
Johan Commelin (May 26 2021 at 11:30):
I had a proof with congr' 5 in it. I changed the associativity in some definition above it. Instead of failing, the congr' now gives me
50 goals
Peter Scholze (May 26 2021 at 11:33):
It's important to have goals :wink:
Scott Morrison (May 26 2021 at 11:34):
Presumably all the goals are sensible things like ℕ = S⁷ ...
Last updated: May 02 2025 at 03:31 UTC