Skip to content

Pull requests: leanprover-community/mathlib4

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

Pull requests list

chore: final batch of mass replacements refine' to refine
#13357 opened May 29, 2024 by adomani Loading…
feat(AlgebraicGeometry/EllipticCurve/Affine): add further map lemmas awaiting-review The author would like community review of the PR t-algebraic-geometry Algebraic geometry t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#13356 opened May 29, 2024 by Multramate Loading…
feat(Topology): some lemmas about continuity of functions out of one point compactifications awaiting-review The author would like community review of the PR t-topology Topological spaces, uniform spaces, metric spaces, filters
#13355 opened May 29, 2024 by dagurtomas Loading…
typo: fix two typos in the docs for global_attribute linter awaiting-review The author would like community review of the PR documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. maintainer-merge
#13354 opened May 29, 2024 by adomani Loading…
2
feat(Analysis/Fourier): discrete Fourier transform on ZMod N
#13353 opened May 29, 2024 by loefflerd Loading…
feat(RingTheory/RootsOfUnity/Complex): complex roots of unity have norm 1 awaiting-review The author would like community review of the PR maintainer-merge t-algebra Algebra (groups, rings, fields etc)
#13352 opened May 29, 2024 by MichaelStollBayreuth Loading…
4
chore: clean up nolints.yml workflow awaiting-review The author would like community review of the PR CI Modifies the continuous integration / deployment setup
#13351 opened May 29, 2024 by grunweg Loading…
feat: add card_divisors theorem awaiting-review The author would like community review of the PR
#13350 opened May 29, 2024 by Jun2M Loading…
Some results about infinite products of the form 1+a_n. WIP Work in progress
#13349 opened May 29, 2024 by CBirkbeck • Draft
feat(GroupTheory/OrderOfElement): equivalences preserve orders awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc)
#13348 opened May 29, 2024 by MichaelStollBayreuth Loading…
6
feat(NumberTheory/LSeries): special values of Hurwitz zeta awaiting-review The author would like community review of the PR t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#13347 opened May 29, 2024 by loefflerd Loading…
3
CI test: nolint update workflow test-ci A label used to help test CI actions WIP Work in progress
#13346 opened May 29, 2024 by grunweg Loading…
1
chore: adaptations for nightly-2024-05-29 awaiting-review The author would like community review of the PR
#13345 opened May 29, 2024 by semorrison Loading…
1
chore: shorten proof of DecompositionMonoid.primal in GCDMonoid.Basic awaiting-review The author would like community review of the PR maintainer-merge
#13344 opened May 29, 2024 by dwrensha Loading…
5
fix(nolints.yml): correct main steps of the update-nolints workflow awaiting-review The author would like community review of the PR CI Modifies the continuous integration / deployment setup
#13343 opened May 29, 2024 by grunweg Loading…
refactor: split Fin.succAboveEmb into an Embedding and an OrderEmbedding awaiting-review The author would like community review of the PR maintainer-merge
#13341 opened May 29, 2024 by Ruben-VandeVelde Loading…
2
refactor: tweak and move functionality for getting all modules out of scripts awaiting-review The author would like community review of the PR
#13339 opened May 29, 2024 by grunweg Loading…
1 task
1
chore(Order): More simp lemmas awaiting-review The author would like community review of the PR t-order Order theory
#13338 opened May 29, 2024 by YaelDillies Loading…
feat: Monotonicity of monadic operations on Part awaiting-review The author would like community review of the PR t-order Order theory
#13337 opened May 29, 2024 by YaelDillies Loading…
chore: deprecate Nat.div_mod_eq_mod_mul_div and Nat.mul_div_mul_comm_of_dvd_dvd awaiting-review The author would like community review of the PR maintainer-merge
#13336 opened May 29, 2024 by dwrensha Loading…
5
feat(LightProfinite): light profinite sets as sequential limits with surjective transition maps blocked-by-other-PR This PR depends on another PR to Mathlib
#13333 opened May 29, 2024 by dagurtomas Loading…
1 task
1
feat(RingTheory/GradedAlgebra/HomogeneousLocalization): add HomogeneousLocalization.map awaiting-review The author would like community review of the PR maintainer-merge t-algebra Algebra (groups, rings, fields etc)
#13332 opened May 29, 2024 by jjaassoonn Loading…
3
feat(CategoryTheory/MorphismProperty): the factorization axiom awaiting-review The author would like community review of the PR t-category-theory Category theory
#13331 opened May 29, 2024 by joelriou Loading…
1
fix: rename IsSimpleOrder.LT.lt.eq_bot/top awaiting-review The author would like community review of the PR maintainer-merge
#13330 opened May 29, 2024 by Ruben-VandeVelde Loading…
2
chore(Combinatorics/Additive/PluenneckeRuzsa): Use semantic lemma names awaiting-review The author would like community review of the PR t-combinatorics Combinatorics
#13329 opened May 29, 2024 by YaelDillies Loading…
ProTip! Filter pull requests by the default branch with base:master.