The formalisation of mathematics is continuing rapidly, but combinatorics remains underrepresented, with the field’s reliance on techniques from a wide range of mathematics being one challenge to formalisation efforts. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher’s Inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher’s Inequality.