-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Pull requests: leanprover-community/mathlib4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(Combinatorics/SimpleGraph/Clique): use Combinatorics
IsContained instead of an explicit embedding from top
t-combinatorics
#35613
opened Feb 21, 2026 by
SnirBroshi
Loading…
feat(CategoryTheory/Abelian): the localization w.r.t. a Serre class
t-category-theory
Category theory
#35612
opened Feb 21, 2026 by
joelriou
Loading…
feat(Data/Fin): add several lemmas about subtraction of Data (lists, quotients, numbers, etc)
Fin.{castLT, castAdd, castSucc, castPred}
t-data
#35610
opened Feb 21, 2026 by
IvanRenison
Loading…
chore: deprecate Turing files
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
t-computability
Computability theory (TMs, DFAs, languages, grammars, etc)
#35609
opened Feb 21, 2026 by
BoltonBailey
Loading…
1 task
chore(Computability): move TM files to a single folder
file-removed
A Lean module was (re)moved without a `deprecated_module` annotation
t-computability
Computability theory (TMs, DFAs, languages, grammars, etc)
#35608
opened Feb 21, 2026 by
BoltonBailey
Loading…
fix(Tactic): make Tactics, attributes or user commands
eta_expand idempotent
t-meta
#35607
opened Feb 21, 2026 by
gasparattila
Loading…
feat(NumberTheory/Zsqrtd): add Archimedean instance via toReal
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
large-import
Automatically added label for PRs with a significant increase in transitive imports
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-number-theory
Number theory (also use t-algebra or t-analysis to specialize)
#35606
opened Feb 21, 2026 by
FrankieeW
Loading…
1 task
feat: transfer instances of This PR depends on another PR (this label is automatically managed by a bot)
ContinuousFunctionalCalculus to type synonyms with weaker topologies
blocked-by-other-PR
#35605
opened Feb 21, 2026 by
j-loreaux
Loading…
1 task
chore: deprecate unused norm_cast lemma
t-meta
Tactics, attributes or user commands
#35604
opened Feb 21, 2026 by
DavidLedvinka
Loading…
feat(GroupTheory/Frattini): add more theorems
large-import
Automatically added label for PRs with a significant increase in transitive imports
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-group-theory
Group theory
#35603
opened Feb 21, 2026 by
2500223210-max
Loading…
Add implementation of Kleene's algorithm to show each regular language has a regex matching it
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-computability
Computability theory (TMs, DFAs, languages, grammars, etc)
feat(RingTheory/Lasker): second uniqueness theorem for primary decomposition
blocked-by-other-PR
This PR depends on another PR (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)
t-ring-theory
Ring theory
#35599
opened Feb 21, 2026 by
tb65536
Loading…
1 task
feat(CategoryTheory/Abelian/Exact): add easy lemmas about short exactness
t-category-theory
Category theory
WIP
Work in progress
#35598
opened Feb 21, 2026 by
Paul-Lez
Loading…
feat(AdicTopology): add three lemmas about adic topology
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-topology
Topological spaces, uniform spaces, metric spaces, filters
#35597
opened Feb 21, 2026 by
BryceT233
Loading…
chore(RingTheory/AdicCompletion): update the definition of A reviewer has approved the changed; awaiting maintainer approval.
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-ring-theory
Ring theory
AdicCompletion.map
maintainer-merge
#35595
opened Feb 21, 2026 by
BryceT233
Loading…
feat(RingTheory): This PR depends on another PR (this label is automatically managed by a bot)
t-ring-theory
Ring theory
Extension.CotangentSpace commutes with base change
blocked-by-other-PR
#35594
opened Feb 21, 2026 by
chrisflav
Loading…
1 task
feat(RingTheory/Extension): naive cotangent complex commutes with flat base change
blocked-by-other-PR
This PR depends on another PR (this label is automatically managed by a bot)
t-ring-theory
Ring theory
#35593
opened Feb 21, 2026 by
chrisflav
Loading…
2 tasks
chore(Order/Defs/Unbundled): deprecate Order theory
def Transitive in favor of class IsTrans
t-order
#35592
opened Feb 21, 2026 by
SnirBroshi
Loading…
feat(Algebra): add Algebra (groups, rings, fields, etc)
AlgHom.ulift
t-algebra
#35590
opened Feb 20, 2026 by
chrisflav
Loading…
feat: Topological spaces, uniform spaces, metric spaces, filters
SeparatelyContinuousMul class for multiplication which is continuous in each variable
t-topology
#35589
opened Feb 20, 2026 by
j-loreaux
Loading…
chore(Util/Qq): remove This PR does not pass CI yet. This label is automatically removed once it does.
t-meta
Tactics, attributes or user commands
meta
awaiting-CI
#35588
opened Feb 20, 2026 by
eric-wieser
Loading…
perf(LinearAlgebra/RootSystem/GeckConstruction/Relations): get rid of some This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
t-algebra
Algebra (groups, rings, fields, etc)
aesop
new-contributor
#35587
opened Feb 20, 2026 by
GrigorenkoPV
Loading…
feat(CategoryTheory/Abelian/Preradical): introduce and characterize radicals
blocked-by-other-PR
This PR depends on another PR (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!
t-category-theory
Category theory
#35586
opened Feb 20, 2026 by
farmanb
Loading…
1 task
Previous Next
ProTip!
Follow long discussions with comments:>50.