Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,194 Open 18,870 Closed
1,194 Open 18,870 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
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Chore: Replace open scoped Classical with (open scoped Classical in) or (classical) new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community!
#20501 opened Jan 6, 2025 by kvanvels Loading…
1
chore(NumberTheory/NumberField/AdeleRing): refactor adele rings maintainer-merge t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#20500 opened Jan 5, 2025 by kbuzzard Loading…
3
feat(GroupTheory/MaximalSubgroups): define maximal subgroups t-algebra Algebra (groups, rings, fields, etc)
#20499 opened Jan 5, 2025 by AntoineChambert-Loir Loading…
2
chore: to_additive various results on groups, group actions awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields, etc)
#20498 opened Jan 5, 2025 by AntoineChambert-Loir Loading…
9
chore: generalize more materials about linear independence over semirings blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#20497 opened Jan 5, 2025 by alreadydone Loading…
1 task
2
feat: IsSuccPrelimit a → IsLUB (Iio a) a t-order Order theory
#20496 opened Jan 5, 2025 by vihdzp Loading…
1
Feat(Combinatorics/Nullstellensatz): formalize Alon's Combinatorial Nullstellensatz blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot)
#20495 opened Jan 5, 2025 by AntoineChambert-Loir Loading…
1 task
@YaelDillies
2
feat(AlgebraicGeometry): Π Rᵢ-points of schemes t-algebraic-geometry Algebraic geometry
#20494 opened Jan 5, 2025 by erdOne Loading…
1
chore(SetTheory/Ordinal/Topology): generalize theorems to SuccOrder t-set-theory Set theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#20491 opened Jan 5, 2025 by vihdzp Loading…
1
feat(Algebra/Azumaya/Defs): Define Azumaya 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)
#20489 opened Jan 5, 2025 by Whysoserioushah Loading…
23
feat(Mathlib/Data): setOf_eq_singleton_iff_of_nodup t-data Data (lists, quotients, numbers, etc)
#20488 opened Jan 5, 2025 by LeoDog896 Loading…
6
chore: avoid unnecessary change tactics maintainer-merge
#20486 opened Jan 5, 2025 by kim-em Loading…
13
chore: cleanup many erw
#20484 opened Jan 5, 2025 by kim-em Loading…
9
doc: change "module homomorphism" to "linear map" t-algebra Algebra (groups, rings, fields, etc)
#20481 opened Jan 5, 2025 by trivial1711 Loading…
4
chore(LinearIndependent): generalize to semirings t-algebra Algebra (groups, rings, fields, etc)
#20480 opened Jan 5, 2025 by alreadydone Loading…
7
feat(Aesop): Make some SetLike rules unsafe, add new SetLike rules t-algebra Algebra (groups, rings, fields, etc)
#20477 opened Jan 5, 2025 by artie2000 Loading…
9
refactor: redefine Subrel in terms of α → Prop instead of Set α t-order Order theory
#20475 opened Jan 4, 2025 by vihdzp Loading…
1 task done
10
refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in AddCommGrp large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#20474 opened Jan 4, 2025 by smorel394 Loading…
19
feat(ContDiff): add iteratedFDeriv_comp t-analysis Analysis (normed *, calculus)
#20472 opened Jan 4, 2025 by urkud Loading…
1
feat(RingTheory/Smooth): calculate H¹(L) via formally smooth extensions t-algebra Algebra (groups, rings, fields, etc)
#20471 opened Jan 4, 2025 by erdOne Loading…
1
feat(1000): fill in more entries documentation Improvements or additions to documentation
#20470 opened Jan 4, 2025 by YaelDillies Loading…
4
feat: Sherman Morrison formula for rank 1 update of the matrix inverse t-data Data (lists, quotients, numbers, etc)
#20466 opened Jan 4, 2025 by MohanadAhmed Loading…
1
feat(LowerUpperTopology): add lemmas t-order Order theory t-topology Topological spaces, uniform spaces, metric spaces, filters
#20465 opened Jan 4, 2025 by urkud Loading…
1
feat(ContinuousMultilinearMap): add lemmas about .prod delegated t-analysis Analysis (normed *, calculus)
#20462 opened Jan 4, 2025 by urkud Loading…
14
feat(LocalRing/Module): fg flat module over a local ring is free blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
#20460 opened Jan 4, 2025 by alreadydone Loading…
1 task
2
ProTip! Follow long discussions with comments:>50.