Zulip Chat Archive

Stream: maths

Topic: Snake Lemma

Ken Lee (Aug 11 2020 at 13:46):

Is the snake lemma for abelian categories in mathlib yet?

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.

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: Dec 20 2023 at 11:08 UTC