Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,185 Open 18,975 Closed
1,185 Open 18,975 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(Combinatorics/SetFamily/AhlswedeZhang): golf simp t-combinatorics Combinatorics
#20598 opened Jan 9, 2025 by LeoDog896 Loading…
1
chore: clean up some erw in cyclotomic polynomials t-algebra Algebra (groups, rings, fields, etc)
#20597 opened Jan 9, 2025 by kim-em Loading…
1
chore(Asymptotics/TVS): golf t-analysis Analysis (normed *, calculus)
#20596 opened Jan 9, 2025 by urkud Loading…
1
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 fields from UniqueContinuousFunctionalCalculus 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…
1
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
chore(RingTheory/Ideal/Quotient): shorten proof of ringCon.mul' t-algebra Algebra (groups, rings, fields, etc)
#20586 opened Jan 8, 2025 by dwrensha Loading…
1
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…
9
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
feat: a ∈ s ^ n iff there exists a sequence f of n elements of s such that ∏ i, f i = a t-algebra Algebra (groups, rings, fields, etc)
#20580 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: pointwise set operations commute with cartesian product delegated t-algebra Algebra (groups, rings, fields, etc)
#20579 opened Jan 8, 2025 by YaelDillies Loading…
5
feat(Asymptotics): prove IsLittleOTVS.add t-analysis Analysis (normed *, calculus)
#20578 opened Jan 8, 2025 by urkud • Draft
7
chore: make FooHom.coe_id a norm_cast lemma
#20576 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: (C a * p).leadingCoeff = a * p.leadingCoeff t-algebra Algebra (groups, rings, fields, etc)
#20575 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: If s ∆ t is finite, then s ∆ u is finite iff t ∆ u is awaiting-CI t-data Data (lists, quotients, numbers, etc)
#20574 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: ⨅ i, f i ≤ ⨆ i, f i awaiting-author A reviewer has asked the author a question or requested changes
#20573 opened Jan 8, 2025 by YaelDillies Loading…
4
feat: sets of doubling strictly less than 3/2 large-import Automatically added label for PRs with a significant increase in transitive imports t-combinatorics Combinatorics
#20572 opened Jan 8, 2025 by YaelDillies Loading…
2
ProTip! Type g i on any issue or pull request to go back to the issue listing page.