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
Jakob

[1] http://afp.sourceforge.net/entries/Rank_Nullity_Theorem.shtml


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...
>
>
> reagrds
> yongjian Li
>
> 2014-04-09
>
>
>
> lyj238
>



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