Little octopi :octopus:

Stream: general

[Simon Hudon]

I just noticed that, when searching the mathlib documentation, a series of octopi come parading on the screen. This is funny! Should we credit @Gabriel Ebner for that idea?