Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,895 Open 30,078 Closed
1,895 Open 30,078 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(MeasureTheory/VectorMeasure): remove use of erw in toMeasureOfLEZero_apply t-measure-probability Measure theory / Probability theory
#32539 opened Dec 7, 2025 by euprunin Loading…
1
chore(Algebra/Homology/HomotopyCategory): remove use of erw in shiftIso_hom_app and shiftIso_inv_app t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32538 opened Dec 7, 2025 by euprunin Loading…
1
feat(RingTheory): strongly transcendental elements t-ring-theory Ring theory
#32537 opened Dec 7, 2025 by erdOne Loading…
1
feat(RingTheory): descend finiteness along quotients by nilpotent ideals t-ring-theory Ring theory
#32536 opened Dec 7, 2025 by erdOne Loading…
1
feat(CategoryTheory): the opposite of a triangulated category is triangulated t-category-theory Category theory
#32535 opened Dec 7, 2025 by joelriou Loading…
1
feat(RingTheory): algebraic Zariski main theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-ring-theory Ring theory WIP Work in progress
#32534 opened Dec 7, 2025 by erdOne Loading…
7 tasks
2
feat(Algebra/Polynomial/Roots): Add ofMultiset_injective 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)
#32533 opened Dec 7, 2025 by metakunt Loading…
1
feat(Combinatorics/SimpleGraph/Connectivity): connected components are maximally connected subsets/subgraphs t-combinatorics Combinatorics
#32532 opened Dec 7, 2025 by SnirBroshi Loading…
1
feat(Combinatorics/SimpleGraph): Konig’s theorem on bipartite graphs new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#32531 opened Dec 7, 2025 by ksenono Loading…
1
feat(Topology): basic properties of discrete sets t-topology Topological spaces, uniform spaces, metric spaces, filters
#32530 opened Dec 7, 2025 by erdOne Loading…
1
feat(RingTheory): the etale locus of an algebra t-ring-theory Ring theory
#32529 opened Dec 7, 2025 by erdOne Loading…
1
feat(RingTheory): going-down for integrally closed domains
#32528 opened Dec 7, 2025 by erdOne Loading…
1
chore(LinearAlgebra/PiTensorProduct): remove use of erw in nonempty_lifts and liftAux_tprod 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)
#32527 opened Dec 7, 2025 by PrParadoxy Loading…
1
chore(LinearAlgebra/Multilinear/Basic.lean): remove erws in restr 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)
#32526 opened Dec 7, 2025 by PrParadoxy Loading…
1
chore(Data/Num): remove uses of erw in of_to_nat' t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32522 opened Dec 6, 2025 by euprunin Loading…
1
refactor: generalize semicontinuity file-removed A Lean module was (re)moved without a `deprecated_module` annotation t-topology Topological spaces, uniform spaces, metric spaces, filters
#32521 opened Dec 6, 2025 by j-loreaux Loading…
2
feat(AlgebraicTopology): stability properties of monomorphisms in the category of simplicial sets blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#32517 opened Dec 6, 2025 by joelriou Loading…
1 task
2
feat(CategoryTheory): monomorphisms in Type are stable under coproducts t-category-theory Category theory
#32515 opened Dec 6, 2025 by joelriou Loading…
2
feat(Algebra/Polynomial): add grind annotations for C_mul_monomial and monomial_mul_C t-algebra Algebra (groups, rings, fields, etc)
#32513 opened Dec 6, 2025 by euprunin Loading…
3
chore: update Mathlib dependencies 2025-12-06 dependency-bump This PR bumps the version of an upstream dependency (but not toolchain).
#32512 opened Dec 6, 2025 by mathlib4-update-dependencies-bot Loading…
1
chore(Geometry/RingedSpace/PresheafedSpace): remove use of erw in colimitCocone maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebraic-geometry Algebraic geometry tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32510 opened Dec 6, 2025 by euprunin Loading…
5
feat(Algebra/MonoidAlgebra): single as a DistribMulActionHom t-algebra Algebra (groups, rings, fields, etc)
#32508 opened Dec 6, 2025 by YaelDillies Loading…
1
chore(LinearAlgebra/ExteriorAlgebra): remove use of erw in map_surjective_iff maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32507 opened Dec 6, 2025 by euprunin Loading…
3
chore(ModelTheory): remove use of erw in comp t-logic Logic (model theory, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32506 opened Dec 6, 2025 by euprunin Loading…
1
chore(Algebra/DirectSum): remove use of erw in mul_eq_dfinsuppSum maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#32503 opened Dec 6, 2025 by euprunin Loading…
3
ProTip! Exclude everything labeled bug with -label:bug.