-
Notifications
You must be signed in to change notification settings - Fork 297
Issues: leanprover-community/mathlib
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Author
Label
Projects
Milestones
Assignee
Sort
Issues list
Etale cohomology
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
long term
#1142
opened Jun 21, 2019 by
kbuzzard
Miracle Flatness and Zariski's Main Theorem
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#4014
opened Sep 1, 2020 by
adomani
transporting definitions and theorems along isomorphisms.
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
t-meta
Tactics, attributes or user commands
#408
opened Oct 8, 2018 by
kbuzzard
Expand the surreals library
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
help-wanted
The author needs attention to resolve issues
#1046
opened May 18, 2019 by
rwbarton
homological algebra
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
roadmap
#1063
opened May 20, 2019 by
semorrison
6 of 11 tasks
RFC: turn Request for comment
mul_action
into a structure
needs-refactor
RFC
#1117
opened Jun 7, 2019 by
urkud
documenting mathlib
help-wanted
The author needs attention to resolve issues
long term
needs-documentation
This PR is missing required documentation
#1260
opened Jul 24, 2019 by
robertylewis
Probably This issue is a feature request, either for mathematics, tactics, or CI
t-meta
Tactics, attributes or user commands
setup_tactic_parser
can be integrated to use open_locale
instead
feature-request
#1465
opened Sep 20, 2019 by
khoek
Define Banach algebras
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#1858
opened Jan 6, 2020 by
urkud
2 of 5 tasks
Tactic to transfer theorems / definitions using an equivalence.
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
t-meta
Tactics, attributes or user commands
#1868
opened Jan 8, 2020 by
urkud
Formal roadmaps need to be explained and documented
needs-documentation
This PR is missing required documentation
#2016
opened Feb 19, 2020 by
jcommelin
1 of 2 tasks
Document This PR is missing required documentation
_eta
, _beta
etc in naming
needs-documentation
#2102
opened Mar 7, 2020 by
urkud
Define exact sequences
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#2179
opened Mar 18, 2020 by
TwoFX
Linter
doc_blame
generates unwanted warning when using old_structure_cmd
bug
#2409
opened Apr 13, 2020 by
ocfnash
Linear programming
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
please-adopt
This PR/issue may have been abandoned by the original contributor. You are welcome to take it over.
#2601
opened May 5, 2020 by
jcommelin
More on quotients of categories
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#2710
opened May 17, 2020 by
rwbarton
push_hom
and pull_hom
tactics
feature-request
#2725
opened May 18, 2020 by
semorrison
Write a tactic to copy a structure while updating some fields.
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
t-meta
Tactics, attributes or user commands
#1847
opened Jan 2, 2020 by
urkud
Previous Next
ProTip!
Mix and match filters to narrow down what you’re looking for.