A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem
Crossref DOI link: https://doi.org/10.1007/s10817-016-9379-z
Published Online: 2016-06-14
Published Print: 2017-04
Update policy: https://doi.org/10.1007/springer_crossmark_policy
Aransay, Jesús http://orcid.org/0000-0002-4079-8307
Divasón, Jose
Funding for this research was provided by:
Universidad de La Rioja (FPI-UR-12)
Ministerio de Economía y Competitividad (ES) (MTM2014-54151-P)
License valid from 2016-06-14