Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Issues: leanprover-community/mathlib3

Clear current search query, filters, and sorts
91 Open 271 Closed
91 Open 271 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
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

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
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 _eta, _beta etc in naming needs-documentation This PR is missing required documentation
#2102 opened Mar 7, 2020 by urkud
Quadratic forms over Q_p feature-request This issue is a feature request, either for mathematics, tactics, or CI
#2553 opened Apr 28, 2020 by jcommelin
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
push_hom and pull_hom tactics feature-request This issue is a feature request, either for mathematics, tactics, or CI help-wanted The author needs attention to resolve issues t-meta Tactics, attributes or user commands
#2725 opened May 18, 2020 by kim-em
integrate noncomm_ring and ring t-meta Tactics, attributes or user commands
#2880 opened May 31, 2020 by kim-em
apply_congr with h enhancement t-meta Tactics, attributes or user commands
#2882 opened May 31, 2020 by kim-em
Port convexity to affine spaces enhancement
#2910 opened Jun 1, 2020 by urkud
5 of 16 tasks
Document rw configuration needs-documentation This PR is missing required documentation t-meta Tactics, attributes or user commands
#3095 opened Jun 17, 2020 by PatrickMassot
a non-interactive version of squeeze_simp, for use by other tactics needs-refactor t-meta Tactics, attributes or user commands
#3120 opened Jun 20, 2020 by kim-em
document derive / derive_handler attributes help-wanted The author needs attention to resolve issues needs-documentation This PR is missing required documentation
#3533 opened Jul 24, 2020 by bryangingechen
properties of ring homomorphisms feature-request This issue is a feature request, either for mathematics, tactics, or CI
#4013 opened Sep 1, 2020 by jcommelin
47 of 96 tasks
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
Unify char_zero with char_p needs-refactor
#4688 opened Oct 19, 2020 by urkud
Redefine linear_map.tensor to be a bundled hom
#4906 opened Nov 4, 2020 by Vierkantor
@[simps] improvements enhancement t-meta Tactics, attributes or user commands
#5489 opened Dec 24, 2020 by fpvandoorn
7 of 18 tasks
@fpvandoorn
Add a user command to print the declarations in the current file
#7003 opened Apr 2, 2021 by alexjbest
@alexjbest
Predicate for Kan extensions feature-request This issue is a feature request, either for mathematics, tactics, or CI medium
#7051 opened Apr 6, 2021 by b-mehta
Lemmas produced by @[elementwise] aren't usable in Type
#7189 opened Apr 14, 2021 by kim-em
to_additive-like attribute for order_dual feature-request This issue is a feature request, either for mathematics, tactics, or CI t-meta Tactics, attributes or user commands
#7691 opened May 22, 2021 by bryangingechen
fin_cases for finsets not as versatile as multiset and list t-meta Tactics, attributes or user commands
#10248 opened Nov 9, 2021 by alexjbest
Add an @[intuit] attribute or similar
#10954 opened Dec 21, 2021 by eric-wieser
Make to_ring_hom_eq_coe into a simp lemma in ring_equiv
#11186 opened Jan 2, 2022 by mcdoll
Limits and continuity for real.logb feature-request This issue is a feature request, either for mathematics, tactics, or CI good-first-project
#11388 opened Jan 12, 2022 by BoltonBailey
ProTip! Type g i on any issue or pull request to go back to the issue listing page.