is _ in mathlib?

Stream: mathlib4

[Emily Riehl]

I had a vague memory that there might be a thread to ask whether a certain result is in mathlib. Where is it?

In my case, I'm specifically interesting in the equivalence between a category C and the slice category C/T (called "Over T") in the case where T is a terminal object.

[Matthew Ballard]

#Is there code for X?

[Patrick Massot]

There is whole channel devoted to this, called Is there code for X?

[Patrick Massot]

And Matthew was faster

[Matthew Ballard]

Plus a link ;)

[Matthew Ballard]

But I don't have the power to move anything

[Emily Riehl]

Thanks. I knew it was somewhere.

[Matthew Ballard]

Also, less authoritatively, I cannot find that equivalence with a quick search

[Matthew Ballard]

docs#subterminalEquivMonoOverTerminal might be useful to look at though