Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Sign up
Appearance settings
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Pull requests: leanprover-community/mathlib3

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
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort

Pull requests list

chore(*): add mathlib4 synchronization comments awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. mathlib4-synchronization This PR *only* adds a message to the module doc about synchronization with mathlib4
#19240 opened Aug 20, 2023 by github-actions bot Loading...
feat(order/filter,topology/instances/nnreal): upgrade some lemmas to iff awaiting-author A reviewer has asked the author a question or requested changes modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-order Order hierarchy t-topology Topological spaces, uniform spaces, metric spaces, filters too-late This PR was ready too late for inclusion in mathlib3
#18964 opened May 7, 2023 by urkud Loading...
feat(ring_theory/integral_domain): generalize card_fiber_eq_of_mem_range awaiting-author A reviewer has asked the author a question or requested changes modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. t-algebra Algebra (groups, rings, fields etc) too-late This PR was ready too late for inclusion in mathlib3
#17653 opened Nov 20, 2022 by urkud Loading...
feat(tactic/recommend): recommend tactic based on premise selection modifies-tactic-syntax This PR adds a new interactive tactic or modifies the syntax of an existing tactic. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 t-meta Tactics, attributes or user commands
#16807 opened Oct 4, 2022 by gebner Loading...
feat(analysis/inner_product_space/reproducing_kernel): Reproducing kernel Hilbert spaces awaiting-author A reviewer has asked the author a question or requested changes t-analysis Analysis (normed *, calculus) too-late This PR was ready too late for inclusion in mathlib3
#16351 opened Sep 2, 2022 by shingtaklam1324 Loading...
feat(topology/sheaves/*): sheaves have enough injectives under some condition t-algebraic-geometry Algebraic geometry too-late This PR was ready too late for inclusion in mathlib3 WIP Work in progress
#15742 opened Jul 28, 2022 by jjaassoonn • Draft
11 tasks done
ProTip! Updated in the last three days: updated:>2025年10月22日.

AltStyle によって変換されたページ (->オリジナル) /