Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,291 Open 33,223 Closed
2,291 Open 33,223 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

feat(FieldTheory/RatFunc): Lüroth's theorem
#36109 opened Mar 4, 2026 by justus-springer Loading…
5 tasks
1
feat(Algebra/Polynomial/Eval/Subring): not_mem_map_range t-algebra Algebra (groups, rings, fields, etc)
#36108 opened Mar 4, 2026 by justus-springer Loading…
1
chore: mark definitions outputting classes as implicit_reducible
#36107 opened Mar 4, 2026 by sgouezel Loading…
1
chore(Analysis/InnerProductSpace): remove a hypothesis from LinearMap.IsSymmetric.card_filter_eigenvalues_eq t-analysis Analysis (normed *, calculus)
#36106 opened Mar 4, 2026 by nielsvoss Loading…
1
chore(Algebra): shorten, style t-algebra Algebra (groups, rings, fields, etc)
#36105 opened Mar 4, 2026 by LLaurance Loading…
1
feat(CategoryTheory/Endofunctor/Algebra): add Adámek's initial algebra theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-category-theory Category theory
#36104 opened Mar 4, 2026 by LarsenClose Loading…
2
feat(Algebra/MvPolynomial/CharacteristicSet): add Characteristic Set 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)
#36103 opened Mar 4, 2026 by SnkXyx Loading…
2
feat(RingTheory): flat extension of local ring t-ring-theory Ring theory
#36102 opened Mar 4, 2026 by Thmoas-Guan • Draft
2
feat(RingTheory): lemmas about power of maximal ideal t-ring-theory Ring theory
#36101 opened Mar 4, 2026 by wwylele Loading…
1
feat(FieldTheory/KrullTopology): generalize theorems t-algebra Algebra (groups, rings, fields, etc)
#36100 opened Mar 4, 2026 by plp127 Loading…
1
feat(Combinatorics/SimpleGraph/Sum): edgeSet equivalence blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-combinatorics Combinatorics
#36099 opened Mar 4, 2026 by SnirBroshi Loading…
1 task
2
chore: make psuedoparents of algebraic substructures reducible
#36097 opened Mar 4, 2026 by matthewjasper Loading…
1
chore: remove stray comment about backward.isDefEq.respectTransparency
#36095 opened Mar 4, 2026 by kim-em Loading…
4
feat(GroupTheory/Nilpotent): remove [IsNilpotent] assumption from some theorems t-algebra Algebra (groups, rings, fields, etc) t-group-theory Group theory
#36093 opened Mar 4, 2026 by tb65536 Loading…
1
feat(CategoryTheory/Monoidal/Cartesian/Grp_): Grp has kernels large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#36092 opened Mar 3, 2026 by tb65536 Loading…
2
feat(Analysis.LocallyConvex.Separation): add Eidelheit's separation theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#36091 opened Mar 3, 2026 by JJYYY-JJY Loading…
8
feat(Topology/Compactness/CompactSystem): set system of finite unions of sets in a compact system is again a compact system
#36089 opened Mar 3, 2026 by pfaffelh Loading…
1
feat: add a LE version of previous div_lt_div_iff_mul_lt_mul theorem 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)
#36088 opened Mar 3, 2026 by pevogam Loading…
2
chore: fix diamonds for Real/Complex Algebra instances
#36087 opened Mar 3, 2026 by matthewjasper Loading…
2
feat: add liftEquiv for groups, rings, algebras, and adjoin roots merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#36086 opened Mar 3, 2026 by Multramate Loading…
2
Eliminated a hypothesis on IsTheta.rpow new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#36084 opened Mar 3, 2026 by emo916math Loading…
2
feat: decomposition of ContinuousAffineMap as an Equiv
#36083 opened Mar 3, 2026 by gasparattila Loading…
1
feat(CategoryTheory/Sites): being subcanonical is reflected by full faithful continuous functors t-category-theory Category theory
#36082 opened Mar 3, 2026 by chrisflav Loading…
1
refactor(CategoryTheory/Sites): redefine the category of sheaves using ObjectProperty.FullSubcategory large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-category-theory Category theory WIP Work in progress
#36081 opened Mar 3, 2026 by joelriou Loading…
1
chore: adapt names after #34658 ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
#36080 opened Mar 3, 2026 by MichaelStollBayreuth Loading…
@jcommelin
2
ProTip! Follow long discussions with comments:>50.