Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,633 Open 24,390 Closed
1,633 Open 24,390 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

fix(RefinedDiscrTree): remove funny transparency handling t-meta Tactics, attributes or user commands
#26531 opened Jun 30, 2025 by JovanGerb Loading…
1
feat(Geometry/Euclidean/Incenter): signs of barycentric coordinates of touchpoints blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) t-euclidean-geometry Affine and axiomatic geometry
#26530 opened Jun 29, 2025 by jsm28 Loading…
3 tasks
2
feat(Geometry/Euclidean/Projection): projection onto a 0-simplex blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) easy < 20s of review time. See the lifecycle page for guidelines. t-euclidean-geometry Affine and axiomatic geometry
#26529 opened Jun 29, 2025 by jsm28 Loading…
1 task
2
feat(Geometry/Euclidean/Sphere/Tangent): lemmas about points in subspace easy < 20s of review time. See the lifecycle page for guidelines. t-euclidean-geometry Affine and axiomatic geometry
#26528 opened Jun 29, 2025 by jsm28 Loading…
1
feat(LinearAlgebra/AffineSpace/Independent): faceOpposite point in 1-simplex easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#26527 opened Jun 29, 2025 by jsm28 Loading…
1
eat(RingTheory/Valuation/IntegrallyClosed): the valuation subring is integrally closed 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-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#26526 opened Jun 29, 2025 by pechersky Loading…
4 tasks
2
chore(RingTheory/Valuation): Valution.Integers implies IsFractionRing t-algebra Algebra (groups, rings, fields, etc)
#26524 opened Jun 29, 2025 by pechersky Loading…
1
chore: split out NatCast Complex instance easy < 20s of review time. See the lifecycle page for guidelines. t-data Data (lists, quotients, numbers, etc)
#26522 opened Jun 29, 2025 by Ruben-VandeVelde Loading…
1
chore(Algebra/BigOperators): rename variables away from greek letters awaiting-CI t-algebra Algebra (groups, rings, fields, etc)
#26521 opened Jun 29, 2025 by YaelDillies Loading…
1
feat(Algebra/Homology): truncations of ConnectData.cochainComplex large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc) t-category-theory Category theory
#26520 opened Jun 29, 2025 by joelriou Loading…
1
Von Neumann awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-set-theory Set theory
#26518 opened Jun 29, 2025 by knalasol Loading…
@kckennylau
30
feat(LinearAlgebra): complementary submodule under submodule easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#26513 opened Jun 29, 2025 by wwylele Loading…
1
feat(RingTheory/Valuation/Integers): nontrivial_iff easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc) t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#26512 opened Jun 29, 2025 by pechersky Loading…
1
feat(RingTheory/Valuation): le_one_of_subsingleton easy < 20s of review time. See the lifecycle page for guidelines. t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#26511 opened Jun 29, 2025 by pechersky Loading…
1
feat(Matroid): exchange lemmas involving closure t-combinatorics Combinatorics t-data Data (lists, quotients, numbers, etc)
#26510 opened Jun 29, 2025 by alreadydone Loading…
1
feat(RingTheory/Valuation): IsNontrivial.exists_one_lt t-algebra Algebra (groups, rings, fields, etc) t-analysis Analysis (normed *, calculus) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#26509 opened Jun 29, 2025 by pechersky Loading…
1
feat(Polynomial): Monic.C_ne_zero easy < 20s of review time. See the lifecycle page for guidelines. t-algebra Algebra (groups, rings, fields, etc)
#26508 opened Jun 29, 2025 by pechersky Loading…
2
feat(Algebra/Polynomial/Degree/IsMonicOfDegree): new file t-algebra Algebra (groups, rings, fields, etc)
#26507 opened Jun 29, 2025 by MichaelStollBayreuth Loading…
@riccardobrasca
1
feat: smooth Riemannian bundles t-differential-geometry Manifolds etc
#26506 opened Jun 29, 2025 by sgouezel Loading…
1
feat: in a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm t-topology Topological spaces, uniform spaces, metric spaces, filters
#26505 opened Jun 29, 2025 by sgouezel Loading…
1
feat: the image of an interval under a continuous monotone map is an interval t-topology Topological spaces, uniform spaces, metric spaces, filters
#26504 opened Jun 29, 2025 by sgouezel Loading…
1
feat: constructor for emetric space with a preexisting topology large-import Automatically added label for PRs with a significant increase in transitive imports t-topology Topological spaces, uniform spaces, metric spaces, filters
#26503 opened Jun 29, 2025 by sgouezel Loading…
1
feat: monotonicity of lineMap maintainer-merge t-analysis Analysis (normed *, calculus)
#26502 opened Jun 29, 2025 by sgouezel Loading…
7
feat: more API on manifolds t-differential-geometry Manifolds etc
#26501 opened Jun 29, 2025 by sgouezel Loading…
@grunweg
10
feat: more properties of the manifold structure on Icc t-differential-geometry Manifolds etc
#26500 opened Jun 29, 2025 by sgouezel Loading…
@grunweg
10
ProTip! Follow long discussions with comments:>50.