Skip to content

Pull requests: leanprover-community/mathlib4

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
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

Pull requests list

chore: golf using grw blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports
#26981 opened Jul 10, 2025 by JovanGerb Loading…
1 task
feat(Algebra/GroupWithZero/WithZero): add lemma map'_surjective_iff delegated t-algebra Algebra (groups, rings, fields, etc)
#26980 opened Jul 10, 2025 by faenuccio Loading…
feat(Topology/GDelta/Basic): add lemmas about unions of meagre sets awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters
#26979 opened Jul 10, 2025 by shalliso Loading…
feat: induction principle for open sets according to a basis delegated t-topology Topological spaces, uniform spaces, metric spaces, filters
#26978 opened Jul 10, 2025 by YaelDillies Loading…
refactor(Order/Concept): rename intentClosurelowerPolar t-order Order theory
#26976 opened Jul 10, 2025 by vihdzp Loading…
feat: a norm_num extension for complex numbers awaiting-author A reviewer has asked the author a question or requested changes. t-meta Tactics, attributes or user commands
#26975 opened Jul 10, 2025 by Whysoserioushah Loading…
feat(Geometry/Diffeology): diffeologies generated from sets of plots blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-differential-geometry Manifolds etc
#26973 opened Jul 10, 2025 by peabrainiac Loading…
1 task
feat(CategoryTheory): localization of quotient categories t-category-theory Category theory
#26972 opened Jul 10, 2025 by joelriou Loading…
feat(Order/Concept): sets in a concept are codisjoint blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-order Order theory
#26968 opened Jul 10, 2025 by vihdzp Loading…
1 task
feat(AlgebraicTopology/ModelCategory): left homotopies blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory WIP Work in progress
#26967 opened Jul 10, 2025 by joelriou Loading…
1 task
feat: the Dedekind-MacNeille completion t-order Order theory
#26966 opened Jul 10, 2025 by vihdzp Draft
feat: add root system induction principle equivalent to connectedness of Dynkin diagram t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#26965 opened Jul 10, 2025 by ocfnash Loading…
chore: remove whitespace maintainer-merge
#26963 opened Jul 10, 2025 by adomani Loading…
feat(Data/Nat/Fib/Basic): some API for Nat.fib new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#26962 opened Jul 10, 2025 by themathqueen Loading…
feat(RingTheory/PowerSeries/Substitution): add API t-algebra Algebra (groups, rings, fields, etc)
#26961 opened Jul 10, 2025 by mariainesdff Loading…
feat(AlgebraicTopology/ModelCategory): the lemma by K. S. Brown blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory WIP Work in progress
#26960 opened Jul 10, 2025 by joelriou Loading…
2 tasks
feat(AlgebraicTopology): path objects in model categories blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory WIP Work in progress
#26958 opened Jul 10, 2025 by joelriou Loading…
1 task
feat(Algebra): unmixed thm of Cohen-Macaulay ring blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#26957 opened Jul 10, 2025 by Thmoas-Guan Loading…
1 task
feat(LinearAlgebra/OnSup): extend linear maps to sums of modules awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc)
#26955 opened Jul 10, 2025 by mariainesdff Loading…
chore: use edist instead of dist in TendstoInMeasure t-measure-probability Measure theory / Probability theory
#26954 opened Jul 10, 2025 by RemyDegenne Loading…
feat(CategoryTheory/DayConvolution): monoid objects internal to day convolutions blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#26952 opened Jul 9, 2025 by robin-carlier Loading…
1 task
ProTip! no:milestone will show everything without a milestone.