Re: [isabelle] formalization of linear algebra in Isabelle
Dear Yongjian Li,
There is a formalization of the "dimension formula" for linear maps 
which makes use of the "Multivariate Analysis" library of HOL. I guess you
can use the theory to discover which parts of linear algebra are already
formalized and which are not.
2014-04-09 13:14 GMT+02:00 lyj238 <lyj238 at gmail.com>:
> Dear experts:
> Do you know some work on linear algebra formalization in Isabelle,
> e.g., matrix...
> yongjian Li
This archive was generated by a fusion of
Pipermail (Mailman edition) and