This repository contains a Lean formalisation of Improved Lower Bounds for Strong n-Conjectures by Rupert Hölzl, Sören Kleine and Frank Stephan. The documentation may be viewed here.
The name Redhill is a location and corresponding MRT station in Singapore.
Upstreaming PRs to mathlib
- #36098, #35673 (computability and order properties of
radicalforℕ, ℤ) - #36340 (
Int.mul_{pos,nonpos,neg}_iff) - #36488 (
Finset.disjoint_preimage– eventually found unnecessary) - #36799 (miscellaneous lemmas, including
n ≤ primorial n) - #36948 (lemmas for
IsCoprimeandIsRelPrime)