mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
The set `{x | p x}` belongs to `f` iff `∀ s, {x | x ∈ s → p x} ∈ f`. Specialization for `EventuallyEq` and `Eventually.LE`. Suggested by @urkud....
Adds API for localizing algebra maps, in general form and specialized to `IsLocalization.Away`. Also shows that localization commutes with kernels. --- [](https://gitpod.io/from-referrer/)
This PR introduces the `#min_imps` command. Writing `#min_imps stx` scans the syntax `stx` to find a collection of minimal imports that should be sufficient for `stx` to make sense. If...
The density of a finite set in an ambient group is a quantity of great interest in combinatorics. This PR defines `Finset.dens s` for `s : Finset α` as the...
Add the q-expansion of the cotangent function that will be needed for Eisenstein series q-expansions. --- - [x] depends on: #12758 - [x] depends on: #12771 [](https://gitpod.io/from-referrer/)
This PR renames the `no_lost_declarations` script to `decls_diff`, to better describe the effect of the script. It was originally intended as a script to make sure that "moving" PRs did...
Add some lemmas and equivs relating to orbits for and quotients by the action of a subgroup. From AperiodicMonotilesLean. --- [](https://gitpod.io/from-referrer/)
Infrastructure for working with [monomial orders](https://en.wikipedia.org/wiki/Monomial_order) on MvPolynomial rings. The lexicographic order is used in #6593 (proof of the fundamental theorem of symmetric polynomials) --- [](https://gitpod.io/from-referrer/)
Given a short exact short complex `S` in an abelian category `C` and `A : C`, we construct a long exact sequence `LargeExact A S.X₁ n₀ ⟶ LargeExact A S.X₂...
Given a short exact short complex `S` in an abelian category `C` and `B : C`, we construct the contravariant (exact) sequence of `LargeExt` `LargeExact S.X₃ B n₀ ⟶ LargeExact...