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(IntegrableOn): generalise one more section to enorms carleson part of the ongoing formalization of Carleson's theorem t-measure-probability Measure theory / Probability theory
#27419 opened Jul 24, 2025 by grunweg Loading…
wip(Intervalintegral): generalise more lemmas to enorms t-measure-probability Measure theory / Probability theory
#27418 opened Jul 24, 2025 by grunweg Loading…
feat: add SigmaCompleteLattice t-order Order theory
#27417 opened Jul 24, 2025 by PierreQuinton Loading…
feat(Algebra/Homology): Ext modules blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory WIP Work in progress
#27416 opened Jul 24, 2025 by joelriou Loading…
1 task
feat(ModelTheory): Semilinear sets in are closed under intersection and complement blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-logic Logic (model theory, etc)
#27414 opened Jul 24, 2025 by staroperator Loading…
3 of 6 tasks
chore: fix create-adaptation-pr.sh script
#27413 opened Jul 24, 2025 by kim-em Loading…
feat(Valued/LocallyCompact): do not require RankOne to show IsDVR blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#27412 opened Jul 24, 2025 by pechersky Loading…
1 task
feat(GroupTheory/ArchimedeanDensely): locally finite linearly ordered groups are mul archimedean awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory
#27410 opened Jul 24, 2025 by pechersky Loading…
chore: generalize typeclass assumptions on DFinsupp SMul maintainer-merge t-data Data (lists, quotients, numbers, etc)
#27409 opened Jul 23, 2025 by eric-wieser Loading…
feat(Topology/ClusterPt): Swapped version of ClusterPt.frequently t-topology Topological spaces, uniform spaces, metric spaces, filters
#27407 opened Jul 23, 2025 by tb65536 Loading…
feat(MeasureTheory/Measure/AddContent): Add lemma addContent_biUnion_eq t-measure-probability Measure theory / Probability theory
#27406 opened Jul 23, 2025 by tb65536 Loading…
fix(to_additive): expand kernel projections to use reorder t-meta Tactics, attributes or user commands
#27405 opened Jul 23, 2025 by JovanGerb Loading…
feat: replace probably erroneous usage of ⬝ (with old \cdot) by · (with \centerdot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#27403 opened Jul 23, 2025 by MoritzBeroRoos Loading…
fix: delete a duplicate instance easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)
#27402 opened Jul 23, 2025 by eric-wieser Loading…
fix: make compile_inductive% work correctly with new compiler new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-meta Tactics, attributes or user commands
#27401 opened Jul 23, 2025 by zwarich Loading…
feat: define geometrically reduced algebras 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)
#27400 opened Jul 23, 2025 by dleijnse Loading…
feat: replace every usage of ⬝ᵥ (with old \cdot) by ·ᵥ (with \centerdot) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#27399 opened Jul 23, 2025 by MoritzBeroRoos Loading…
chore(*): fix some scattered adaptation notes ready-to-merge This PR has been sent to bors. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#27396 opened Jul 23, 2025 by Vierkantor Loading…
feat(Algebra/Homology): the canonical t-structure on the derived category t-category-theory Category theory WIP Work in progress
#27395 opened Jul 23, 2025 by joelriou Loading…
feat(Tactic/SimpUtils): add simproc finding commands t-meta Tactics, attributes or user commands
#27392 opened Jul 23, 2025 by Paul-Lez Loading…
feat(CategoryTheory/Limits/Shapes/Pullback/Categorical): pseudofunctoriality structure of categorical pullback squares blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-category-theory Category theory
#27391 opened Jul 23, 2025 by robin-carlier Loading…
1 task
feat(FieldTheory/Galois): normal basis theorem blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc) WIP Work in progress
#27390 opened Jul 23, 2025 by alreadydone Loading…
2 tasks
chore(Analysis): remove a few unneccessary assignments in instance declarations ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
#27389 opened Jul 23, 2025 by Vierkantor Loading…
ProTip! Adding no:label will show everything without a label.