Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,914 Open 30,810 Closed
1,914 Open 30,810 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: mark Ordinal.enumOrd with no_expose awaiting-CI This PR doesn't pass CI yet. This label is automatically removed once it does. easy < 20s of review time. See the lifecycle page for guidelines. t-set-theory Set theory
#33298 opened Dec 26, 2025 by vihdzp Loading…
1
feat(Algebra/Polynomial/Roots): add card_rootSet_le large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#33297 opened Dec 26, 2025 by tb65536 Loading…
1
feat(LinearAlgebra/GeneralLinearGroup/Center): center of the general linear group blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#33296 opened Dec 26, 2025 by AntoineChambert-Loir Loading…
1 task
3
feat(Algebra/Central/End): center of endomorphisms of a free module t-algebra Algebra (groups, rings, fields, etc)
#33295 opened Dec 26, 2025 by AntoineChambert-Loir Loading…
1
refactor: deprecate Ordinal.IsNormal for Order.IsNormal t-order Order theory t-set-theory Set theory
#33294 opened Dec 26, 2025 by vihdzp Loading…
1
ci(daily.yml): only run notify jobs in leanprover-community/mathlib4 CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.
#33293 opened Dec 26, 2025 by bryangingechen Loading…
1
feat(Combinatorics/SimpleGraphs/LineGraph): lift copies/isomorphisms to line-graph large-import Automatically added label for PRs with a significant increase in transitive imports
#33292 opened Dec 25, 2025 by SnirBroshi Loading…
1
refactor(Computability): File for state transition systems t-computability Computability theory (TMs, DFAs, languages, grammars, etc)
#33291 opened Dec 25, 2025 by BoltonBailey Loading…
1
chore: golf using grind and simp
#33290 opened Dec 25, 2025 by euprunin Loading…
3
feat(Analysis/SpecialFunctions/Integrals): add ∫ x : ℝ in a..b, (c ^ 2 + x ^ 2)⁻¹ new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#33289 opened Dec 25, 2025 by michelsol Loading…
1
chore(Combinatorics/SimpleGraph/Paths): review API t-combinatorics Combinatorics
#33288 opened Dec 25, 2025 by vihdzp Loading…
1
feat(CategoryTheory/Sites): more API for IsSheafFor t-category-theory Category theory
#33287 opened Dec 25, 2025 by joelriou Loading…
1
chore: golf using grind
#33286 opened Dec 25, 2025 by euprunin Loading…
1
chore(*): golf, add missing lemmas
#33285 opened Dec 25, 2025 by urkud Loading…
3
doc(RingTheory): fix file refs t-ring-theory Ring theory
#33284 opened Dec 25, 2025 by harahu • Draft
1
feat(Polynomial/Chebyshev): Differential equations for T and U t-ring-theory Ring theory
#33283 opened Dec 25, 2025 by YuvalFilmus Loading…
1
feat(LinearAlgebra/Center): description of the center of the algebra of endomorphisms blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#33282 opened Dec 25, 2025 by AntoineChambert-Loir Loading…
1 task
5
feat(Analysis/SpecialFunctions/Integrals): integral of 1/sqrt(1-x^2) and its integrability. 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!
#33281 opened Dec 25, 2025 by michelsol Loading…
1 task
2
feat(MeasureTheory/Integral/IntervalIntegral): add variant integral_deriv_eq_sub_uIoo of 2nd theorem of calculus. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory
#33280 opened Dec 25, 2025 by michelsol Loading…
1
doc(LinearAlgebra): fix file refs t-algebra Algebra (groups, rings, fields, etc)
#33279 opened Dec 25, 2025 by harahu Loading…
1
doc(MeasureTheory): fix file refs t-measure-probability Measure theory / Probability theory
#33278 opened Dec 25, 2025 by harahu Loading…
1
doc(Logic): fix file refs t-logic Logic (model theory, etc)
#33277 opened Dec 25, 2025 by harahu Loading…
1
feat: Renaming List.reverse_perm to List.reverse_perm_self new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#33276 opened Dec 25, 2025 by NicolaBernini Loading…
1
feat(Trigonometric/Chebyshev/Extremal): Chebyshev polynomials maximize iterated derivatives blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33275 opened Dec 25, 2025 by YuvalFilmus Loading…
2 tasks
2
feat(LinearAlgebra/Lagrange): Formula for iterated derivative of a polynomial using Lagrange interpolation blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#33274 opened Dec 25, 2025 by YuvalFilmus Loading…
3 tasks
2
ProTip! Follow long discussions with comments:>50.