Zulip Chat Archive
Stream: condensed mathematics
Topic: is_zero sorries
Adam Topaz (Apr 18 2022 at 20:15):
The file for_mathlib/sheafification_mono has a few sorries about proving that certain things satisfy is_zero. They should be mostly straightforward if anybody wants to take a look. This file will be used for the proof of Prop 2.1
Johan Commelin (Apr 18 2022 at 20:33):
I pushed some miniwip
Johan Commelin (Apr 19 2022 at 07:24):
Only the first two sorrys are left.
Johan Commelin (Apr 19 2022 at 07:56):
That file is now sorry-free.
Yaël Dillies (Apr 19 2022 at 08:03):
There is_zero sorry
Last updated: Dec 20 2023 at 11:08 UTC