Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
2,014 Open 29,259 Closed
2,014 Open 29,259 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: remove unused Decidable* instances in theorem types
#31831 opened Nov 19, 2025 by thorimur Loading…
1
feat(LinearAlgebra/Matrix): Existence of Singular Value Decomposition 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)
#31830 opened Nov 19, 2025 by CodeTitanium Loading…
7
refactor(GroupTheory/SpecificGroups/Cyclic): clean up statement of classification of abelian finite simple groups t-group-theory Group theory
#31829 opened Nov 19, 2025 by tb65536 Loading…
5
feat: add getD_comp_some lemma for Option type t-data Data (lists, quotients, numbers, etc)
#31828 opened Nov 19, 2025 by BoltonBailey Loading…
1
fix: revert change to devcontainer for short-term fix for Codespaces
#31826 opened Nov 19, 2025 by StevenClontz • Draft
1
feat: add splitOnP_append_cons t-data Data (lists, quotients, numbers, etc)
#31825 opened Nov 19, 2025 by BoltonBailey Loading…
1
chore: turn on module system in MathlibTest maintainer-merge A reviewer has approved the changed; awaiting maintainer approval.
#31823 opened Nov 19, 2025 by thorimur Loading…
5
feat: privateModule linter blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-linter Linter
#31820 opened Nov 19, 2025 by thorimur Loading…
1 task
20
perf: de-instance some WithLp norm structures used for type synonyms awaiting-author A reviewer has asked the author a question or requested changes. bench-after-CI Once the PR passes CI, comment `!bench` on the PR t-analysis Analysis (normed *, calculus)
#31819 opened Nov 19, 2025 by j-loreaux Loading…
3
feat: add grind annotations for Set.mem_toFinset and Multiset.mem_toFinset
#31818 opened Nov 19, 2025 by euprunin Loading…
1
chore: remove extra monic hypotheses from divByMonic and modByMonic lemmas t-algebra Algebra (groups, rings, fields, etc) t-ring-theory Ring theory
#31817 opened Nov 19, 2025 by kckennylau Loading…
9
chore(Order/Defs/PartialOrder): fix naming of DecidableLE' t-order Order theory
#31816 opened Nov 19, 2025 by JovanGerb Loading…
1
feat(CMField): add IsCyclotomicExtension.Rat.isCMField blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot)
#31812 opened Nov 19, 2025 by xroblot Loading…
2 tasks
2
chore(CMField): generalize definitions and results blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#31811 opened Nov 19, 2025 by xroblot Loading…
1 task
2
chore(TotallyReal/TotallyComplex): remove the NumberField hypothesis t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#31810 opened Nov 19, 2025 by xroblot Loading…
1
feat: differentiation of test function as a CLM blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#31809 opened Nov 19, 2025 by ADedecker Loading…
1 task
2
chore(Order/Def): avoid relying on internal class projections in other files
#31808 opened Nov 19, 2025 by JovanGerb Loading…
@bryangingechen
1
feat(CategoryTheory/Cat/Basic): API for converting between 2-morphisms in Cat and natural transformations. t-category-theory Category theory
#31807 opened Nov 19, 2025 by edegeltje • Draft
1
feat: endow test functions with the natural LF topology blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-analysis Analysis (normed *, calculus)
#31806 opened Nov 19, 2025 by ADedecker Loading…
1 task
3
feat(AlgebraicTopology): horns in Δ[n] as multicoequalizers blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#31805 opened Nov 19, 2025 by joelriou Loading…
2 tasks
2
chore(Tactic/Linters): remove public section t-linter Linter
#31803 opened Nov 19, 2025 by grunweg Loading…
9
feat(AlgebraicTopology): horns in Δ[2] as pushouts blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-algebraic-topology Algebraic topology WIP Work in progress
#31802 opened Nov 19, 2025 by joelriou Loading…
1 task
2
chore: make CLM.extend total and define LM.leftInverse awaiting-author A reviewer has asked the author a question or requested changes. t-analysis Analysis (normed *, calculus)
#31799 opened Nov 19, 2025 by mcdoll Loading…
3
feat(AlgebraicTopology): multicoequalizers and pushouts of simplicial sets t-algebraic-topology Algebraic topology
#31797 opened Nov 19, 2025 by joelriou Loading…
3
feat(Data/Real/EReal): add mul_lt_mul_of_pos_left theorem new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-data Data (lists, quotients, numbers, etc)
#31796 opened Nov 19, 2025 by dobronx1325 Loading…
1
ProTip! no:milestone will show everything without a milestone.