Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,520 Open 23,302 Closed
1,520 Open 23,302 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: adaptations for nightly-2025-05-29
#25306 opened May 30, 2025 by leanprover-community-mathlib4-bot Loading…
1
feat(Algebra): small lemmas for taylor 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)
#25305 opened May 29, 2025 by kckennylau Loading…
1
feat(Analysis/Calculus/FDeriv): continuous differentiability from continuous partial derivatives on an open domain in a product space new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus)
#25304 opened May 29, 2025 by igorkhavkine Loading…
1
feat: lint against using native_decide t-linter Linter
#25297 opened May 29, 2025 by grunweg Loading…
8
feat: Add high-level generalizations from MonoidHom lifts 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)
#25296 opened May 29, 2025 by linesthatinterlace Loading…
2 tasks
2
feat: the ConvexCone generated by a set blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-convex-geometry Affine geometry, cones, simplices toric Part of the ongoing formalisation of toric varieties
#25292 opened May 29, 2025 by YaelDillies Loading…
1 task
2
chore(Geometry/Convex/Cone/Basic): clean up t-convex-geometry Affine geometry, cones, simplices toric Part of the ongoing formalisation of toric varieties
#25291 opened May 29, 2025 by YaelDillies Loading…
1
feat: Low-level derivatives of lifts on OneHom, MulHom and MonoidHom 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)
#25290 opened May 29, 2025 by linesthatinterlace Loading…
1 task
3
feat(CategoryTheory): generalize Discrete to arbitrary morphism levels t-category-theory Category theory
#25288 opened May 29, 2025 by robertmaxton42 Loading…
1
feat(Bicategory/CatEnriched): 2-cat from Cat-enriched cat infinity-cosmos This PR is associated with Infinity Cosmos project t-category-theory Category theory
#25287 opened May 29, 2025 by digama0 Loading…
12
feat: define the Lie algebra associated to a root system 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)
#25285 opened May 28, 2025 by ocfnash Loading…
1 task
3
feat(LinearAlgebra/Contraction): bijectivity of dualTensorHom + generalize to CommSemiring t-algebra Algebra (groups, rings, fields, etc)
#25284 opened May 28, 2025 by alreadydone Loading…
2
feat: regular local rings 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-algebra Algebra (groups, rings, fields, etc)
#25283 opened May 28, 2025 by Brian-Nugent Loading…
2 tasks
2
feat: krull dimension facts for Noetherian local rings 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-algebra Algebra (groups, rings, fields, etc)
#25282 opened May 28, 2025 by Brian-Nugent Loading…
1 task
2
chore: automatic removal of empty lines maintainer-merge
#25281 opened May 28, 2025 by adomani Loading…
3
feat: add IsLocalRing.EmbDim, the embedding dimension of a local ring 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)
#25280 opened May 28, 2025 by Brian-Nugent Loading…
15
feat: range of lifts large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#25276 opened May 28, 2025 by eric-wieser Loading…
3
feat: left-tensoring a linear map by a tensor product t-algebra Algebra (groups, rings, fields, etc) toric Part of the ongoing formalisation of toric varieties
#25274 opened May 28, 2025 by YaelDillies Loading…
3
feat: Finsupp.linearCombination MonoidAlgebra.of = id large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#25273 opened May 28, 2025 by YaelDillies Loading…
4
feat: IsClopen.of_thickening_subset_self t-topology Topological spaces, uniform spaces, metric spaces, filters
#25272 opened May 28, 2025 by j-loreaux Loading…
1
feat: promote an AlgEquiv preserving counit and comul to a BialgEquiv t-algebra Algebra (groups, rings, fields, etc) toric Part of the ongoing formalisation of toric varieties
#25271 opened May 28, 2025 by YaelDillies Loading…
1
feat: counit (antipode a) = counit a t-algebra Algebra (groups, rings, fields, etc) toric Part of the ongoing formalisation of toric varieties
#25267 opened May 28, 2025 by YaelDillies Loading…
7
feat: add path component of the identity in a locally path connected topological group, as an open normal subgroup t-topology Topological spaces, uniform spaces, metric spaces, filters
#25266 opened May 28, 2025 by j-loreaux Loading…
1
feat(Order/SupClosed): compl_image_latticeClosure and compl_image_latticeClosure_eq_of_compl_image_eq_self t-order Order theory
#25265 opened May 28, 2025 by FMLJohn Loading…
7
feat: add elementary lifts for OneHom, MulHom and MonoidHom t-algebra Algebra (groups, rings, fields, etc)
#25264 opened May 28, 2025 by linesthatinterlace Loading…
5
ProTip! Add no:assignee to see everything that’s not assigned.