finished my first “serious” formalization (i.e. it’s an actual theorem, not a toy example). this is based on an example from the book i’m reading (Mathematics in Lean) but i rewrote the code on my own from scratch to better understand the proof.

it was fun! (and took me the whole week)