lean_work

Current work in Lean -- translating matrix.v from Mathematical Components Coq library, formalizing miscellaneous quantum theory math, formalizing synthetic differential geometry, formalizing quantum lambda calculus