-
Notifications
You must be signed in to change notification settings - Fork 891
Pull requests: leanprover-community/mathlib4
Author
Label
Projects
Milestones
Reviews
Assignee
Sort
Pull requests list
feat(FaaDiBruno): add estimates on the difference between taylor series
#31937
opened Nov 22, 2025 by
urkud
Loading…
feat: allow Algebra (groups, rings, fields, etc)
grind to unfold abs
t-algebra
#31935
opened Nov 22, 2025 by
kim-em
Loading…
feat(NumberTheory): Gelfond–Schneider Theorem
new-contributor
This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#31931
opened Nov 22, 2025 by
mkaratarakis
Loading…
feat(Data/List/Basic): Data (lists, quotients, numbers, etc)
idxOf lemmas
t-data
#31930
opened Nov 22, 2025 by
SnirBroshi
Loading…
feat: replace
Finsupp.embDomain_apply with more general lemma
#31929
opened Nov 22, 2025 by
kim-em
Loading…
2 tasks
feat: grind annotation for Embedding.injective
t-logic
Logic (model theory, etc)
#31928
opened Nov 22, 2025 by
kim-em
Loading…
feat(Topology): étalé space associated to a predicate on sections
t-topology
Topological spaces, uniform spaces, metric spaces, filters
#31925
opened Nov 21, 2025 by
alreadydone
Loading…
feat(Algebra/Ring/HuntingtonAlgebra): alternative constructions of boolean algebras
t-algebra
Algebra (groups, rings, fields, etc)
t-ring-theory
Ring theory
WIP
Work in progress
#31924
opened Nov 21, 2025 by
AntoineChambert-Loir
•
Draft
feat: Data (lists, quotients, numbers, etc)
Finsupp.embSigma {k : κ} (f : ι k →₀ M) : (Σ k, ι k) →₀ M
t-data
#31923
opened Nov 21, 2025 by
kim-em
Loading…
feat(EqHaar): add < 20s of review time. See the lifecycle page for guidelines.
t-measure-probability
Measure theory / Probability theory
addHaar_nnreal_smul
easy
#31922
opened Nov 21, 2025 by
urkud
Loading…
feat: FiniteExhaustion
t-data
Data (lists, quotients, numbers, etc)
#31921
opened Nov 21, 2025 by
DavidLedvinka
Loading…
feat(RingTheory): integrally closed subring of a field is intersection of valuation subrings
t-ring-theory
Ring theory
WIP
Work in progress
#31919
opened Nov 21, 2025 by
alreadydone
Loading…
chore(Algebra): make invertibleInv an instance
t-algebra
Algebra (groups, rings, fields, etc)
#31916
opened Nov 21, 2025 by
alreadydone
Loading…
refactor: clean up occurances of Algebra (groups, rings, fields, etc)
Splits (p.map (RingHom.id _))
t-algebra
#31915
opened Nov 21, 2025 by
tb65536
Loading…
chore: deprecate all remaining modules in < 20s of review time. See the lifecycle page for guidelines.
t-analysis
Analysis (normed *, calculus)
tech debt
Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip
Analysis/NormedSpace
easy
#31913
opened Nov 21, 2025 by
j-loreaux
Loading…
chore(Algebra): change two statements in CubicDiscriminant
maintainer-merge
A reviewer has approved the changed; awaiting maintainer approval.
t-algebra
Algebra (groups, rings, fields, etc)
#31912
opened Nov 21, 2025 by
alreadydone
Loading…
feat(MeasureTheory): ae-measurability notation wrt non-standard sigma-algebra
easy
< 20s of review time. See the lifecycle page for guidelines.
t-measure-probability
Measure theory / Probability theory
#31910
opened Nov 21, 2025 by
YaelDillies
Loading…
chore(MeasureTheory): mark < 20s of review time. See the lifecycle page for guidelines.
t-measure-probability
Measure theory / Probability theory
map_dirac as simp
easy
#31909
opened Nov 21, 2025 by
YaelDillies
Loading…
Previous Next
ProTip!
Adding no:label will show everything without a label.