Zulip Chat Archive

Stream: maths

Topic: Snake Lemma

view this post on Zulip Ken Lee (Aug 11 2020 at 13:46):

Is the snake lemma for abelian categories in mathlib yet?

view this post on Zulip Kevin Buzzard (Aug 11 2020 at 17:05):

There was some excitement about a diagram chasing tactic which existed in some preliminary form but I'm not sure if it made it into mathlib.

view this post on Zulip Johan Commelin (Aug 14 2020 at 12:24):

It's not there yet, but there are bits of progress about every week. @Markus Himmel I guess you are close to starting to PR the tactic, aren't you?

Last updated: May 06 2021 at 17:38 UTC