Five lemma

Stream: Is there code for X?

[Christian Merten]

Do we have the five lemma (https://en.wikipedia.org/wiki/Five_lemma) somewhere?

[Markus Himmel]

docs#CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono

[Christian Merten]

Nice, thanks!

[Kim Morrison]

(Typing "five lemma" in the search box in VSCode produces this. Loogle and the docs are great, but the search box is best. :-)

[Christian Merten]

Not using VS code: is the search box just source code search? (I should just rip grep mathlib source code more often)

[Eric Wieser]

I'd argue that the search box in VSCode is great only for english, and awful for searching by the statement itself. Loogle is a huge step up there.

[Kim Morrison]

Search box with regexps is still superior to loogle for me. :-) Sometime you have to permute the chunks between your .*s, but so much faster workflow wise.

[Yaël Dillies]

Kim Morrison said:

(Typing "five lemma" in the search box in VSCode produces this. Loogle and the docs are great, but the search box is best. :-)

It used to work in the docs, though :sad: