I recently came across the Natural Number Game, the formalization of the proof of PFR over $\mathbb{F}_2$, Functional Programming in Lean, and a few other resources or talks about Lean, so I finally decided to get my hands dirty with it. My first idea was to check Mathlib to see what people have been working on. My favorite hello-world-ish thing in math is the Fibonacci numbers, so I started reading the source for Nat.I learnt of this idea 2 days ago while I was chatting with the MATH201 TA after a recitation, complaining about the absurdity of the course showing matrices before linear transformations.
TL;DR: Given an abelian group $V$ and a field $F$, if we can find a ring homomorphism $\phi:F\to\mathrm{End}(V)$, then $V$ forms a vector space over $F$ when we define $av:=\phi(a)(v)$.
Note: Everything mentioned here works for modules as well as vector spaces by just substituting a ring for the field.Hi, I'm [o̞ɫ'd͡ʒɑj.o̞'ɾɑnso̞j].
CS @ Sabancı ‘26.