[mizar] the rank + nullity = dimension theorem in the mml

[Jesse Alama <alama@stanford.edu>]

I'm currently working on formalizing in mizar Poincaré's proof of
Euler's polyhedron formula ("V-E+F=2").  Poincaré's proof uses the
"rank + nullity = dimension" theorem, which says that for a linear
transformation T from a finite-dimensional vector space U to a
finite-dimensional vector space V we have

  dim(U) = dim(im(T)) + dim(ker(T)),

where im(T) is the image of T in V and ker(T) is the null space of T.
I've hunted in the MML for a formalization of this theorem or
something like it, but, as far as I can see, this theorem isn't in the
MML.  Have any of you come across this theorem, or carried out a
formalization of it?  If so, please let me know; otherwise, I'll soon
start working on formalization of this theorem.

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*393: Incorrect beginning of a reasoning item