Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,186 Open 19,238 Closed
1,186 Open 19,238 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore(Order/WellFoundedSet): get rid of nonrec easy < 20s of review time. See the lifecycle page for guidelines. t-order Order theory
#20862 opened Jan 20, 2025 by vihdzp Loading…
1
feat: notation3-defined pretty printers now make tokens that are clickable in documentation t-meta Tactics, attributes or user commands
#20861 opened Jan 20, 2025 by kmill Loading…
2
chore(Algebra/CharP): prime_ringChar and isPrimePow_card easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#20860 opened Jan 19, 2025 by pechersky Loading…
1
feat: generalize tangent cone lemmas to TVS t-analysis Analysis (normed *, calculus)
#20859 opened Jan 19, 2025 by eric-wieser Loading…
1
feat: make PMF.binomial computable blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot)
#20858 opened Jan 19, 2025 by eric-wieser Loading…
1 task
2
feat: make Sub ℝ≥0 and Sub ℝ≥0∞ computable maintainer-merge
#20856 opened Jan 19, 2025 by eric-wieser Loading…
6
feat: regularity of the pullback of a vector field on a manifold t-differential-geometry Manifolds etc
#20853 opened Jan 19, 2025 by sgouezel Loading…
1
chore(Logic/Equiv/Basic): extend sumCompl API t-data Data (lists, quotients, numbers, etc) t-logic Logic (model theory, etc)
#20850 opened Jan 19, 2025 by vihdzp Loading…
1
chore(Logic/Basic): deprecate proof equalities t-logic Logic (model theory, etc)
#20849 opened Jan 19, 2025 by vihdzp Loading…
2
chore: split Mathlib.Order.Filter.Ultrafilter
#20848 opened Jan 19, 2025 by Ruben-VandeVelde Loading…
5
feat(Logic/Basic): HEq (cast h a) b ↔ HEq a b easy < 20s of review time. See the lifecycle page for guidelines. t-logic Logic (model theory, etc)
#20847 opened Jan 19, 2025 by vihdzp Loading…
1
feat(Polynomial): polynomial sequences are bases for R[X] t-algebra Algebra (groups, rings, fields, etc)
#20846 opened Jan 19, 2025 by Julian Loading…
1
refactor(RingTheory): split off heavy results from Mathlib/RingTheory/Spectrum/*/Basic.lean t-algebra Algebra (groups, rings, fields, etc)
#20845 opened Jan 19, 2025 by mistarro Loading…
1
feature(Analysis/LocallyConvex/Polar): Bipolar theorem large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus) WIP Work in progress
#20843 opened Jan 19, 2025 by mans0954 • Draft
1
feat: add (AE)Measurable.complex_ofReal and fun_prop attributes t-measure-probability Measure theory / Probability theory
#20842 opened Jan 19, 2025 by RemyDegenne Loading…
1
feat: Functor.prod' is final awaiting-author A reviewer has asked the author a question or requested changes t-category-theory Category theory WIP Work in progress
#20841 opened Jan 19, 2025 by TwoFX Loading…
2
feat(CategoryTheory): Subpresheaf is a complete lattice t-category-theory Category theory
#20840 opened Jan 19, 2025 by joelriou Loading…
1
RFC: generalize Disjoint.map t-order Order theory
#20839 opened Jan 19, 2025 by urkud Loading…
1
feat(Combinatorics/SimpleGraph): API for bipartite simple graph double-counting blocked-by-other-PR This PR depends on another PR to Mathlib (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-combinatorics Combinatorics
#20838 opened Jan 19, 2025 by mitchell-horner Loading…
1 task
2
feat(Analysis/SpecialFunctions): prove asymptotic results for binomial coefficents and factorial variants new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#20837 opened Jan 19, 2025 by mitchell-horner Loading…
1
refactor: Abstract out the substructure lattice construction and SetLike closure operators
#20836 opened Jan 18, 2025 by artie2000 • Draft
2
chore(Data/Fin/Basic): split off rev lemmas t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#20833 opened Jan 18, 2025 by BoltonBailey Loading…
1
chore(Data/List/Basic): split off Map2 lemmas t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#20832 opened Jan 18, 2025 by BoltonBailey Loading…
1
feat(Combinatorics/SimpleGraph): Characterizing SimpleGraph.IsCycles t-combinatorics Combinatorics
#20830 opened Jan 18, 2025 by pimotte Loading…
20
feat(RingTheory/Artinian): rewrite results using spectra types instead of sets large-import Automatically added label for PRs with a significant increase in transitive imports new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-algebra Algebra (groups, rings, fields, etc)
#20828 opened Jan 18, 2025 by mistarro Loading…
15
ProTip! Adding no:label will show everything without a label.