mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
This PR adds a new file `NumberTheory.LSeries.Dirichlet` that contains results on L-series of specific functions: * the Möbius function * Dirichlet characters, with the constant function `1` as a special...
These are new lemmas added to the file about proper maps. --- These modifications were done during the conference "Lean for the curious mathematician" 2024. [](https://gitpod.io/from-referrer/)
--- [](https://gitpod.io/from-referrer/)
--- - [x] depends on: #11601 - [x] depends on: #11653 - [x] depends on: #11655 - [x] depends on: #11661 - [x] depends on: #11665 - [x] depends on:...
The bottom part of mathlib is quite a mess. Algebra, data structures and order theory *could* be developed separately (at least for a while) but are not. Instead, "horizontal" imports...
extend more of the API from CountableInterFilter to CardinalInterFilter --- [](https://gitpod.io/from-referrer/)
Take the content of * some of `Algebra.BigOperators.List.Basic` * some of `Algebra.BigOperators.List.Lemmas` * `Algebra.BigOperators.Multiset.Basic` * `Algebra.BigOperators.Multiset.lemmas` * `Algebra.BigOperators.Order` and sort it into six files: * `Algebra.Order.BigOperators.Group.List`. I credit Yakov for...
--- [](https://gitpod.io/from-referrer/)
`Polynomial` and `MvPolynomial` are algebraic objects, hence should be under `Algebra` (or at least not under `Data`) --- [](https://gitpod.io/from-referrer/)
`RCLike` is an analytic typeclass, hence should be under `Analysis` --- [](https://gitpod.io/from-referrer/)