Verification of TR

Stream: new members

[Roman Bacik]

I have started verification of my TR DOI: 10.13140/RG.2.2.27652.59523 here: https://roman3017.github.io/FinLin. Github link there has info on the original TR. It shows that:
Every function on a finite set is a linear function when embedded in a possibly larger ring.
Once done, I would like to contribute it to Mathlib.

My questions are:

• Should people start to formally verify their research?
• Should it be contributed to Mathlib or elsewhere?
• Is there a way to certify passing a formal verification if Mathlib is not the right place?