# Linear Algebraic Techniques in Combinatorics

## Overview
A library for reasoning on linear algebraic techniques for problems on incidence set systems, leading to a formalisation of Fisher's Inequality.

## Linear Algebraic Proof Techniques

Linear algebra plays a critical role in the proof of many important combinatorial theorems. While these techniques are not always obvious to apply, they can result in much cleaner proofs than their traditional combinatorial counter parts, and in some cases are the only current proof available. 

To apply linear algebraic techniques, it is also essential to be able to represent combinatorial structures in a form to which they can be easily applied, such as vectors and matrices. For incidence set systems, the most common linear algebraic representation is Incidence Matrices

## Library History
08/02/2022: Initial public library release. Includes results on incidence systems, design theory extensions, general methods for the rank and linear bound arguments, and form proofs of the odd town theorem, uniform Fisher's inequality, and generalised Fisher's inequality. 
21/04/2022: Major update to the Incidence Matrix representation. This generalised the types used, 
which also enabled significant simplifications to later proofs. This is the version prepared for the AFP entry. 

## Authors
Primary Author is Chelsea Edmonds.
Thanks to Larry Paulson for the useful tips & feedback.