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