# [isabelle] Linear algebra formalisation

I've finished a formalisation of some basic linear algebra *using locales*,
available here:
https://dl.dropboxusercontent.com/u/27883775/work/Isabelle/LinearAlgebra.zip.

It includes (note that some concepts are actually written in module as they
also apply there)

- basic definitions: linear combinations, span, linear independence
- linear transformations
- direct sum of vector spaces, sum of subspaces
- the replacement theorem
- existence of bases in finite-dimensional vector spaces
- rank-nullity theorem

In the process, I also proved some basic facts about rings, modules, and
fields that seem to be missing, as well as finite sums in monoids/modules.

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

As I alluded to in my previous email, I had trouble getting the
automation/simplification to work in my favor, so some of the writeups are
hacky/inconsistent.

[One "hack" I discovered near the end was: to prevent an infinite loop of
simplification from expanding "->" (Pi_I') and trying to show (a x \in
carrier K) by showing it is the image of something in A->B, create a "dummy
definition" Pi2 == Pi, and add simplification rules Pi_simp whose premises
involve Pi2 rather than Pi, and then do:
apply(drule Pi_implies_Pi2)+ (*"flags" all the assumptions piped in so they
aren't expanded.*)