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

% 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{VectorSpace}
\author{Holden Lee\thanks{This work was funded by the Post-Masters Consultancy and the Computer Laboratory at the University of Cambridge.}}
\maketitle

\abstract{
I present a formalisation of basic linear algebra based completely on locales, building off HOL-Algebra. It includes the following:
\begin{enumerate}
\item
basic definitions: linear combinations, span, linear independence
\item
linear transformations
\item
interpretation of function spaces as vector spaces
\item
direct sum of vector spaces, sum of subspaces
\item
the replacement theorem
\item
existence of bases in finite-dimensional vector spaces, definition of dimension
\item
rank-nullity theorem.
\end{enumerate}
Note that some concepts are actually defined and proved for modules as they also apply there.

In the process, I also prove some basic facts about rings, modules, and fields, as well as finite sums in monoids/modules.

Note that infinite-dimensional vector spaces are supported, but dimension is only supported for finite-dimensional vector spaces.

The proofs are standard; the proofs of the replacement theorem and rank-nullity theorem roughly follow the presentation in~\cite{FIS03}. The rank-nullity theorem generalises the existing development in~\cite{AD13} (originally using type classes, now using a mix of type classes and locales).
}

\tableofcontents

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

% generated text of all theories
\input{session}

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

\end{document}

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