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: May 06 2021 at 17:38 UTC