6 citations · 7 across the 7 of their papers we have counts for
Showing 2023Show all
3 papers · 1 filter
math.AG2023
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…
cs.LO2023
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…
cs.LO2023
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…