-
Notifications
You must be signed in to change notification settings - Fork 298
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
Tracking: attribute semireducible/irreducible
mathport
For compatibility with Lean 4 changes, to simplify porting
needs-refactor
#18164
opened Jan 13, 2023 by
jcommelin
The Shapley-Folkman lemma
good-first-project
t-analysis
Analysis (normed *, calculus)
#18135
opened Jan 11, 2023 by
YaelDillies
polyrith
fails if expression is an equality of numerals
bug
t-meta
#17141
opened Oct 24, 2022 by
eric-wieser
Basics of tempered distributions
long term
t-analysis
Analysis (normed *, calculus)
#16386
opened Sep 5, 2022 by
mcdoll
9 of 16 tasks
evaluate This issue is a feature request, either for mathematics, tactics, or CI
int.floor
and int.fract
with norm_num
feature-request
#15992
opened Aug 10, 2022 by
vihdzp
Refactor bilinear forms
RFC
Request for comment
t-algebra
Algebra (groups, rings, fields etc)
#15907
opened Aug 7, 2022 by
mcdoll
2 of 8 tasks
Pi is irrational
good-first-project
t-analysis
Analysis (normed *, calculus)
#15860
opened Aug 4, 2022 by
mcdoll
Cleanup Algebra (groups, rings, fields etc)
direct_sum.sigma_curry
/ direct_sum.is_internal.collected_basis
t-algebra
#15756
opened Jul 29, 2022 by
ADedecker
Remove
has_coe_to_fun
instance for unitary_group
good-first-project
#15749
opened Jul 29, 2022 by
mcdoll
Banach-Alaoglu for topological vector spaces
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#15734
opened Jul 28, 2022 by
mcdoll
expand_exists
improvements
t-meta
#15723
opened Jul 27, 2022 by
robertylewis
Locally convex Hausdorff spaces
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
good-first-project
#15565
opened Jul 20, 2022 by
mcdoll
Add an instance
{add_,}sub{monoid,group}_class S M → has_coe_t S ({add_,}sub{monoid,group} M)
#15053
opened Jun 29, 2022 by
Vierkantor
nth_rewrite incorrectly unifies universe variables
bug
t-meta
Tactics, attributes or user commands
#14994
opened Jun 27, 2022 by
fpvandoorn
apply' can close the goal with metavariables
bug
t-meta
Tactics, attributes or user commands
#14993
opened Jun 27, 2022 by
fpvandoorn
Approximation tactic
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
#14781
opened Jun 16, 2022 by
BoltonBailey
Create library note explaining seemingly redundant
fintype
and decidable
arguments.
#14275
opened May 20, 2022 by
kmill
convert
is_monoid_hom
etc to structures, and move out of deprecated
#13506
opened Apr 19, 2022 by
semorrison
to_
framework
feature-request
#13461
opened Apr 15, 2022 by
YaelDillies
let This issue is a feature request, either for mathematics, tactics, or CI
modifies-tactic-syntax
This PR adds a new interactive tactic or modifies the syntax of an existing tactic.
t-meta
Tactics, attributes or user commands
linear_combination
solve ≠
goals
feature-request
#12685
opened Mar 14, 2022 by
hrmacbeth
Previous Next
ProTip!
Mix and match filters to narrow down what you’re looking for.