Re: [isabelle] formalization of linear algebra in Isabelle

Dear Yongjian Li,

There is a formalization of the "dimension formula" for linear maps [1]
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.

Best regards


2014-04-09 13:14 GMT+02:00 lyj238 <lyj238 at>:

> Dear experts:
>    Do you know some work on linear algebra formalization in Isabelle,
> e.g., matrix...
> reagrds
> yongjian Li
> 2014-04-09
> lyj238

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.