Skip to content

Pull requests: leanprover-community/mathlib4

New pull request New
1,164 Open 18,966 Closed
1,164 Open 18,966 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

feat(Cache): add miniget command
#20568 opened Jan 8, 2025 by grunweg Loading…
3
feat(Cache): two small features
#20567 opened Jan 8, 2025 by grunweg Loading…
11
chore(Algebra/CharP/Defs): do not import Field t-algebra Algebra (groups, rings, fields, etc)
#20566 opened Jan 8, 2025 by YaelDillies Loading…
1
feat: make spanning condition in RootSystem symmetric for roots and coroots. delegated large-import Automatically added label for PRs with a significant increase in transitive imports t-algebra Algebra (groups, rings, fields, etc)
#20564 opened Jan 8, 2025 by ocfnash Loading…
4
feat(Algebra/Group/Even): Clean up file, add Aesop automation t-algebra Algebra (groups, rings, fields, etc)
#20558 opened Jan 7, 2025 by artie2000 Loading…
2
chore(1000.yaml): re-enable comments, small additions and tweaks blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot)
#20554 opened Jan 7, 2025 by grunweg Loading…
1 of 3 tasks
2
chore(Periodic): reduce imports 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)
#20552 opened Jan 7, 2025 by YaelDillies Loading…
1 of 3 tasks
2
perf(ModelTheory/Algebra/Ring/Definability): re-squeeze a slow simp easy < 20s of review time. See the lifecycle page for guidelines. t-logic Logic (model theory, etc)
#20549 opened Jan 7, 2025 by grunweg Loading…
6
chore(Topology/Instances/Real): reduce imports t-topology Topological spaces, uniform spaces, metric spaces, filters
#20548 opened Jan 7, 2025 by YaelDillies Loading…
2
chore: use ofNat more
#20546 opened Jan 7, 2025 by grunweg Loading…
7
feat(Order/Disjointed): allow arbitrary partial orders as domain blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-order Order theory
#20545 opened Jan 7, 2025 by loefflerd Loading…
1 task
2
feat(NumberTheory/NumberField/Basic): ringOfIntegersEquiv API delegated t-number-theory Number theory (also use t-algebra or t-analysis to specialize)
#20544 opened Jan 7, 2025 by kbuzzard Loading…
4
feat(CategoryTheory/Triangulated/Adjunction): the left adjoint of a triangulated functor is triangulated blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports t-category-theory Category theory
#20543 opened Jan 7, 2025 by smorel394 Loading…
1 task
2
chore(LpSpace): move results about the L^p norm earlier t-measure-probability Measure theory / Probability theory
#20541 opened Jan 7, 2025 by YaelDillies Loading…
5
perf: improves the performance of the Repr (Equiv.Perm α) instance (2/4) maintainer-merge t-algebra Algebra (groups, rings, fields, etc)
#20538 opened Jan 7, 2025 by Komyyy Loading…
1 task done
@YaelDillies
8
feat(PrimeSpectrum): clopens in spectra of CommSemirings t-algebra Algebra (groups, rings, fields, etc) t-algebraic-geometry Algebraic geometry
#20533 opened Jan 7, 2025 by alreadydone Loading…
1
feat: test the cache as if in a downstream project CI Modifies the continuous integration / deployment setup
#20532 opened Jan 7, 2025 by kim-em Loading…
1
feat(RingTheory/Idempotents): generalize to Semiring, add Corner and direct product decomposition t-algebra Algebra (groups, rings, fields, etc)
#20531 opened Jan 6, 2025 by alreadydone Loading…
1
refactor(Topology/UniformSpace/Completion): more descriptive names for α → Completion α t-topology Topological spaces, uniform spaces, metric spaces, filters
#20527 opened Jan 6, 2025 by trivial1711 Loading…
4
chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier t-algebra Algebra (groups, rings, fields, etc)
#20526 opened Jan 6, 2025 by YaelDillies Loading…
10
feat(Ringtheory/DedekindDomain/AdicValuation); add mem_integers_of_valuation_le_one delegated t-algebra Algebra (groups, rings, fields, etc)
#20523 opened Jan 6, 2025 by kbuzzard Loading…
8
feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) t-category-theory Category theory
#20522 opened Jan 6, 2025 by smorel394 Loading…
1 of 2 tasks
3
refactor(LinearAlgebra/Lagrange): Remove Lagrange namespace t-algebra Algebra (groups, rings, fields, etc)
#20520 opened Jan 6, 2025 by linesthatinterlace Loading…
1
chore(Algebra/Algebra/Defs): add an algebraMap field to Algebra instead of extending RingHom t-algebra Algebra (groups, rings, fields, etc)
#20518 opened Jan 6, 2025 by edegeltje Loading…
15
feat(Algebra/Module/CharacterModule): a morphism of abelian groups is bijective if and only if its dual is bijective awaiting-author A reviewer has asked the author a question or requested changes t-algebra Algebra (groups, rings, fields, etc)
#20512 opened Jan 6, 2025 by smorel394 Loading…
7
ProTip! What’s not been updated in a month: updated:<2024-12-08.