Kernels Lemma

Stream: Is there code for X?

[Thomas Moulin]

Hi everyone, first contrib to mathlib here!
1 - I am trying to do the kernels lemma from the Missing undergraduate mathematics in mathlib webpage, and wanted to know if someone was already working on this before opening a PR ? I have a working code, but i don't know if it is minimal (I mean I copied and pasted it in the live lean web editor and it works)
2 - Also should I include the corollaries listed on the wikipedia page linked by the Missing undergraduate mathematics in mathlib webpage ? The question is, in order to consider this done all the way should I also do theorems proving : "De plus, la projection de la somme directe V sur V_i parallèlement à ⨁V_j est la restriction à V d'un polynôme en f." (the wikipedia only has a french version for this).

Thanks !

[Niklas Halonen]

The kernels lemma is also mentioned in MIL, but I'm not sure if a version already exists in mathlib as this is not my area of expertise.