Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,215 Open 20,493 Closed
1,215 Open 20,493 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

chore: remove initial space followed by -/
#22158 opened Feb 21, 2025 by adomani Loading…
1
feat(CategoryTheory): any monomorphism in a Grothendieck abelian category is a transfinite composition of pushouts of monomorphisms in a small family large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#22157 opened Feb 21, 2025 by joelriou Loading…
1
chore(Computability): fix naming of lemmas about Sum.inl, Sum.inr, Sum.casesOn t-computability Computability theory (TMs, DFAs, languages, grammars, etc)
#22156 opened Feb 21, 2025 by grunweg Loading…
1
chore: rename {Continuous., continuous_}sum_map to sumMap easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters
#22155 opened Feb 21, 2025 by grunweg Loading…
1
feat: Fintype Ordering easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#22154 opened Feb 21, 2025 by vihdzp Loading…
1
feat: weak approximation theorems for infinite places of a number field large-import Automatically added label for PRs with a significant increase in transitive imports
#22153 opened Feb 21, 2025 by smmercuri Loading…
1 task
1
feat(RingTheory): a semiprimary ring is Noetherian/Artinian iff its Jacobson radical is fg blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#22151 opened Feb 21, 2025 by alreadydone Loading…
1 task
4
chore: more renamings to fit the naming convention
#22148 opened Feb 21, 2025 by grunweg Loading…
1
feat: collections of distinct infinite places contain values that diverge around 1 blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports
#22147 opened Feb 20, 2025 by smmercuri Loading…
1 task
2
chore: split BigOperators/Group t-algebra Algebra (groups, rings, fields, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#22145 opened Feb 20, 2025 by BoltonBailey • Draft
1
feat: collections of non-trivial and pairwise inequivalent absolute values contain values that diverge around 1 blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports
#22142 opened Feb 20, 2025 by smmercuri Loading…
2 tasks
2
chore: separate the automorphism groups from their tautological action blocked-by-other-PR This PR depends on another PR to Mathlib (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)
#22141 opened Feb 20, 2025 by YaelDillies Loading…
1 task
2
feat(Probability): add compProd_sum_(left/right) t-measure-probability Measure theory / Probability theory
#22138 opened Feb 20, 2025 by RemyDegenne Loading…
1
feat: IsEmbedding.sumElim_of_separatingNhds awaiting-author A reviewer has asked the author a question or requested changes t-topology Topological spaces, uniform spaces, metric spaces, filters
#22137 opened Feb 20, 2025 by grunweg Loading…
2
chore(Algebra/GroupPower/IterateHom): move all lemmas earlier t-algebra Algebra (groups, rings, fields, etc)
#22132 opened Feb 20, 2025 by YaelDillies Loading…
3
draft(Module): Module length is additive in short exact sequences blocked-by-other-PR This PR depends on another PR to Mathlib (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! WIP Work in progress
#22127 opened Feb 20, 2025 by Raph-DG Loading…
3 tasks
3
chore(Data/Multiset): split Multiset/Basic.lean into many files awaiting-CI large-import Automatically added label for PRs with a significant increase in transitive imports longest-pole This PR aims to reduce the longest pole in Mathlib t-data Data (lists, quotients, numbers, etc)
#22126 opened Feb 20, 2025 by Vierkantor Loading…
3
feat(Combinatorics/SimpleGraph): define odd components maintainer-merge t-combinatorics Combinatorics
#22125 opened Feb 20, 2025 by pimotte Loading…
7
chore: reorder MulDistribMulAction material blocked-by-other-PR This PR depends on another PR to Mathlib (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) WIP Work in progress
#22121 opened Feb 20, 2025 by YaelDillies Loading…
1 task
5
feat(NumberField/MixedSpace): add polar coordinates change of variables (part 1) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#22120 opened Feb 20, 2025 by xroblot Loading…
1 task
2
feat(Combinatorics/SimpleGraph): part of Tutte's theorem blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-combinatorics Combinatorics
#22119 opened Feb 20, 2025 by pimotte Loading…
1 task
11
feat: Fin.castPred_ne_zero and Pairwise.forall_fin_two large-import Automatically added label for PRs with a significant increase in transitive imports
#22116 opened Feb 20, 2025 by smmercuri Loading…
1
feat(NumberField/MixedSpace): add polar coordinates change of variables (part 2) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) WIP Work in progress
#22115 opened Feb 20, 2025 by xroblot Loading…
1 task
4
chore: norm_cast, simp on AddCircle/Angle
#22112 opened Feb 20, 2025 by LeoDog896 Loading…
1
chore(Algebra/Order/Monoid/Unbundled/WithTop): golf, clean up t-algebra Algebra (groups, rings, fields, etc)
#22109 opened Feb 20, 2025 by YaelDillies Loading…
1
ProTip! What’s not been updated in a month: updated:<2025-01-21.