legendre_QF
Lean code formalizing a proof of Legendre's theorem on diagonal ternary quadratic forms
1-19 of 19 versions of legendre_QF
Sort by
Date
db812acv4.34.0v4.34.01.1 MBdb812acv4.34.0v4.34.01.1 MBf5f331cv4.33.1v4.33.106bd2b7v4.32.2v4.32.2f09d4e4v4.31.0v4.31.01.1 MB3ecebe0v4.30.0v4.30.0d5d70bdv4.29.0v4.29.0843922dv4.28.0v4.28.0ffc076av4.27.0v4.27.0a686ff0v4.26.0v4.26.052d889ev4.25.0v4.25.03590c1dv4.24.0v4.24.07a470b2v4.23.0v4.23.057a0118v4.22.0v4.22.079549d0v4.21.0v4.21.05e1c1b2v4.20.0v4.20.0a93a1fdv4.19.0v4.19.023d6746v4.18.0v4.18.02ba9fbav4.17.0v4.17.0