Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
Clear current search query, filters, and sorts
1,092 Open 12,524 Closed
1,092 Open 12,524 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: golf using List.toArrayMap large-import Automatically added label for PRs with a significant increase in transitive imports
#20613 opened Jan 9, 2025 by grunweg Loading…
1
feat(Algebra/Order/Archimedean/Basic): powers between two elements t-algebra Algebra (groups, rings, fields, etc)
#20612 opened Jan 9, 2025 by MichaelStollBayreuth Loading…
1
chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean easy < 20s of review time. See the lifecycle page for guidelines. t-differential-geometry Manifolds etc
#20611 opened Jan 9, 2025 by grunweg Loading…
1
feat(Topology/Algebra/Algebra/Equiv): continuous algebra equivs t-algebra Algebra (groups, rings, fields, etc) t-topology Topological spaces, uniform spaces, metric spaces, filters WIP Work in progress
#20609 opened Jan 9, 2025 by kbuzzard Loading…
1
feat(Analysis/SpecialFunctions/Pow/Real): add some lemmas t-analysis Analysis (normed *, calculus)
#20608 opened Jan 9, 2025 by MichaelStollBayreuth Loading…
1
algebra map benchmarking WIP Work in progress
#20607 opened Jan 9, 2025 by kbuzzard Loading…
5
doc(Cache): add resp. tweak some documentation documentation Improvements or additions to documentation easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors.
#20606 opened Jan 9, 2025 by grunweg Loading…
2
feat: basic properties of MulExpNegSq and MulExpNegMulSq new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-analysis Analysis (normed *, calculus) t-measure-probability Measure theory / Probability theory
#20604 opened Jan 9, 2025 by JakobStiefel Loading…
2
feat(AlgebraicGeometry): Formally unramified morphisms t-algebraic-geometry Algebraic geometry
#20603 opened Jan 9, 2025 by erdOne Loading…
1
feat(Combinatorics/SimpleGraph): vertices in cycles large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#20602 opened Jan 9, 2025 by pimotte Loading…
5
chore: cleanup more erw t-algebra Algebra (groups, rings, fields, etc)
#20601 opened Jan 9, 2025 by kim-em Loading…
2
chore: ext lemma for DirectSum delegated maintainer-merge t-algebra Algebra (groups, rings, fields, etc)
#20600 opened Jan 9, 2025 by kim-em Loading…
6
chore: use mixin ordered algebraic typeclasses (part 2) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) 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) t-order Order theory WIP Work in progress
#20595 opened Jan 9, 2025 by FR-vdash-bot Loading…
1 task
1
chore: use mixin ordered algebraic typeclasses (part 1) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) 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) t-order Order theory
#20594 opened Jan 9, 2025 by FR-vdash-bot Loading…
1 task
1
feat: mixin ordered algebraic typeclasses 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) t-order Order theory
#20593 opened Jan 9, 2025 by FR-vdash-bot Loading…
1 task
2
chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' t-algebra Algebra (groups, rings, fields, etc)
#20592 opened Jan 9, 2025 by dwrensha Loading…
2
feat(RingTheory): H¹(L) under localization large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#20591 opened Jan 8, 2025 by erdOne Loading…
1
refactor: remove the CompactSpace field from Unique{NonUnital}ContinuousFunctionalCalculus large-import Automatically added label for PRs with a significant increase in transitive imports t-analysis Analysis (normed *, calculus)
#20590 opened Jan 8, 2025 by j-loreaux Loading…
2
feat: AbsoluteValue.IsNontrivial t-analysis Analysis (normed *, calculus)
#20588 opened Jan 8, 2025 by MichaelStollBayreuth Loading…
1
chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty t-algebra Algebra (groups, rings, fields, etc)
#20587 opened Jan 8, 2025 by dwrensha Loading…
2
feat: two lemmas related to Hausdorff distance t-topology Topological spaces, uniform spaces, metric spaces, filters
#20585 opened Jan 8, 2025 by grunweg Loading…
1
feat: commutative semirings satisfy rank condition awaiting-author A reviewer has asked the author a question or requested changes large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#20584 opened Jan 8, 2025 by alreadydone Loading…
18
chore(CategoryTheory): moving/renaming Subpresheaf t-category-theory Category theory
#20583 opened Jan 8, 2025 by joelriou Loading…
1
chore: initialize_simps_projections for Submodule t-algebra Algebra (groups, rings, fields, etc)
#20582 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: Submodule.restrictScalars commutes with pow t-algebra Algebra (groups, rings, fields, etc)
#20581 opened Jan 8, 2025 by YaelDillies Loading…
1
ProTip! Updated in the last three days: updated:>2025-01-06.