mathlib4
mathlib4 copied to clipboard
leanprover-community
The math library of Lean 4
Prove that the product of two `n`-smooth numbers is an `n`-smooth number. Uses two helper lemmas. --- [](https://gitpod.io/from-referrer/)
--- The purpose of this PR is just to bench the "best-case scenario" for a linter which iterates through syntax, updating and checking a simple counter along the way. [
--- Experimental. WIP. Might not be performance-viable. - [ ] depends on: #11519 [](https://gitpod.io/from-referrer/)
We define the class `IsFibered p` which captures what it means for a functor `p : 𝒳 ⥤ 𝒮` to be a fibered category and add some basic API. To...
We define the notion `IsHomLift` which aims to provide API for working with equalities `p(\phi) = f` for a functor `p` and morphisms `\phi`, `f`. This API is extensively used...
We show Eisenstein series are modular forms. --- - [ ] depends on: #12456 [](https://gitpod.io/from-referrer/)
Add some basic results about `ModularGroup.T` relating to slash invariant forms of level Gamma(N) and moving elements into verticalStrips. Needed for #12456 --- [](https://gitpod.io/from-referrer/)
These two trivial lemmas address the following `exact?` failures: ```lean import Mathlib example {x y : ℚ} {m n : ℤ} (hx : 0 ≤ x) (hm : 0 ≤...
I noticed that the following code is surprisingly slow. ``` lean import Mathlib count_heartbeats in example {n : ℕ} : CovariantClass (Fin (n + 1)) (Fin (n + 1)) (·...
There are still some useless lemmas that were simply ported from `Algebra.Order.Monoid.Lemmas`, such as just chain an existing lemma with an assumption and lemmas whose assumptions imply `1 ≤ 0`....