Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] formalization of linear algebra in Isabelle

view this post on Zulip Email Gateway (Aug 19 2022 at 14:15):

From: lyj238 <lyj238@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

view this post on Zulip Email Gateway (Aug 19 2022 at 14:16):

From: Jakob von Raumer <javra@web.de>
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

Last updated: Apr 23 2024 at 16:19 UTC