\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Rank-Nullity Theorem in Linear Algebra}
\author{By Jose Divas\'on and Jes\'us Aransay\thanks{This research has been funded 
  by the research grant FPIUR12 of the Universidad de La Rioja.}}
\maketitle

\begin{abstract}
In this contribution, we present some formalizations based on the HOL-Multivariate-Analysis session of Isabelle. 
Firstly, a generalization of several theorems of such library are presented. Secondly, some definitions 
and proofs involving Linear Algebra and the four fundamental subspaces of a matrix are shown.
Finally, we present a proof of the result known in Linear Algebra as the ``Rank-Nullity Theorem'', 
which states that, given any linear map $f$ from a finite dimensional vector space $V$ to a vector space $W$, 
then the dimension of $V$ is equal to the dimension of the kernel of $f$ (which is a subspace of $V$) and the 
dimension of the range of $f$ (which is a subspace of $W$). The proof presented here is based on the 
one given in \cite{AX97}. As a corollary of the previous theorem, 
and taking advantage of the relationship between linear maps and matrices, we prove that, for every matrix $A$ 
(which has associated a linear map between finite dimensional vector spaces), 
the sum of its null space and its column space (which is equal to the range of the linear map) is equal to 
the number of columns of $A$.
\end{abstract}

\tableofcontents

% sane default for proof documents
\parindent 0pt\parskip 0.5ex

% generated text of all theories
\input{session}

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
