mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Example usage: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/15f08ef06df37286bf8636b4573e84f69994aa4b/PrimeNumberTheoremAnd/PerronFormula.lean#L385-L503. Tools introduced: 1. f =Θ[x -> principal s, y -> any] 1 where f(x, y) = C(x) on compact s 2. 1 =o[x -> any, y ->...
TODO: wait until #12598 has landed (to simplify the diff); use since syntax. --- [](https://gitpod.io/from-referrer/)
This is not exhaustive, but covers ~100 declarations. --- Commits can be reviewed individually. [](https://gitpod.io/from-referrer/)
Work in progress. We aim to prove Ionescu-Tulcea theorem, which implies the existence of a product measure for an arbitrary family of probability measures. --- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
I need these lemmas to prove that Moore graphs of girth 5 are strongly regular. --- - [ ] depends on: #11945 [](https://gitpod.io/from-referrer/)
This defines the diameter of a simple graph, and provides a basic API for it. Co-authored-by: Matt Diamond --- - [ ] depends on: #11945 [](https://gitpod.io/from-referrer/)
In this PR, given a Grothendieck topology `J` on a category `C`, we define a type `J.OneHypercoverFamily` of families of 1-hypercovers. When `H : J.OneHypercoverFamily`, we define a predicate `H.IsGenerating`...
We add a new file `Mathlib.NumberTheory.Cyclotomic.Three` containing various results about the third cyclotomic field. In particular we give a a completely explicit description of the group of units and we...
