6 citations · 7 across the 7 of their papers we have counts for
8 papers
A note on secant defective varieties and Clifford modules
Oliver Nash
We generalise a construction of Landsberg, which associates certain Clifford algebra representations to Severi varieties. We thus obtain a new proof of Russo's Divisibility Propert…
Engel's theorem in Mathlib
Oliver Nash
We discuss the theory of Lie algebras in Lean's Mathlib library. Using nilpotency as the theme, we outline a computer formalisation of Engel's theorem and an application to root sp…
A formalisation of Gallagher's ergodic theorem
Oliver Nash
Gallagher's ergodic theorem is a result in metric number theory. It states that the approximation of real numbers by rational numbers obeys a striking 'all or nothing' behaviour. W…
Formalising the -principle and sphere eversion
Patrick Massot, Floris van Doorn, Oliver Nash
In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existen…
Formalising Lie algebras
Oliver Nash
Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean's Mathlib library. Although b…
K-theory, LQEL manifolds and Severi varieties
Oliver Nash
We use topological K-theory to study non-singular varieties with quadratic entry locus. We thus obtain a new proof of Russo's Divisibility Property for locally quadratic entry locu…
On Klein's Icosahedral Solution of the Quintic
Oliver Nash
We present an exposition of the icosahedral solution of the quintic equation first described in Klein's classic work "Lectures on the icosahedron and the solution of equations of t…
Differential geometry of monopole moduli spaces
Oliver Nash
This thesis was motivated by a desire to understand the natural geometry of hyperbolic monopole moduli spaces. We take two approaches. Firstly we develop the twistor theory of sing…