Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,075 Open 31,693 Closed
2,075 Open 31,693 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore(Analysis/Calculus/FDeriv/Basic): move the lemmas with metrics in their statements to the bottom of the file blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#34348 opened Jan 24, 2026 by eric-wieser Loading…
1 task
2
chore(Analysis/Calculus/FDeriv/Basic): generalize a proof t-analysis Analysis (normed *, calculus)
#34347 opened Jan 24, 2026 by eric-wieser Loading…
1
chore: bump toolchain to v4.27.0 auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#34346 opened Jan 23, 2026 by kim-em Loading…
1
WIP: generalize or comment parts of FDeriv/Basic.lean
#34345 opened Jan 23, 2026 by eric-wieser • Draft
1
chore: don't unfold Pi.single in a simp lemma t-algebra Algebra (groups, rings, fields, etc)
#34344 opened Jan 23, 2026 by eric-wieser Loading…
5
chore(CategoryTheory): dualize NatTrans.Equifibered t-category-theory Category theory
#34343 opened Jan 23, 2026 by erdOne Loading…
1
chore(Analysis/InnerProductSpace/Coalgebra): generalize from NormedRing to Ring t-analysis Analysis (normed *, calculus)
#34341 opened Jan 23, 2026 by themathqueen Loading…
@ocfnash
2
feat(Analysis/SpecialFunctions): BinetFormula part 3 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34340 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(Analysis/SpecialFunctions): BinetFormula part 2 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34339 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(Analysis/SpecialFunctions): BinetFormula part 1 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34338 opened Jan 23, 2026 by jonwashburn Loading…
1 task
3
feat(Analysis/SpecialFunctions/Gamma):add BinetKernel part 3 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34337 opened Jan 23, 2026 by jonwashburn Loading…
1 task
3
feat(Analysis/SpecialFunctions/Gamma):add BinetKernel part 2 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34336 opened Jan 23, 2026 by jonwashburn Loading…
1 task
3
feat(Analysis/SpecialFunctions/Gamma):add BinetKernel part 1 new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34335 opened Jan 23, 2026 by jonwashburn Loading…
6
feat(Analysis/Complex): Cartan inverse factor bound blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34334 opened Jan 23, 2026 by jonwashburn Loading…
2 tasks
2
feat(Analysis/Complex): Hadamard theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34333 opened Jan 23, 2026 by jonwashburn • Draft
1 task
2
feat(Analysis/Complex): more lemmas Hadamard blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34332 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(Analysis/Complex): Hadamard more lemmas blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34331 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(NumberTheory/Height/Basic): add bounds for sums large-import Automatically added label for PRs with a significant increase in transitive imports t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#34330 opened Jan 23, 2026 by MichaelStollBayreuth Loading…
1
feat(Analysis.Complex): Infinite products in topological groups with zero new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34329 opened Jan 23, 2026 by jonwashburn Loading…
3
feat(Analysis/Complex): Hadamard quotient blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34328 opened Jan 23, 2026 by jonwashburn • Draft
10 tasks
3
feat(Analysis/Complex) cartan majorant bound blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34327 opened Jan 23, 2026 by jonwashburn Loading…
2 tasks
3
feat(Analysis/Complex): good radius lemma blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#34326 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(Analysis/Complex): probabilistic radius / averaging lemmas used in proof Hadamard factorization blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34325 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
feat(Analysis/Complex): Log-singularity bounds for Hadamard/Cartan arguments new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34324 opened Jan 23, 2026 by jonwashburn Loading…
1
feat(Analysis/Complex): Zero-free entire functions of polynomial growth are exp of a polynomial blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#34323 opened Jan 23, 2026 by jonwashburn Loading…
1 task
2
ProTip! Add no:assignee to see everything that’s not assigned.