-
Notifications
You must be signed in to change notification settings - Fork 268
Issues: leanprover-community/mathlib4
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 issue for slow Tactics, attributes or user commands
field_simp
calls replaced by simp
t-meta
#15486
opened Aug 4, 2024 by
grunweg
wrong link for Complex.abs in documentation
documentation
Improvements or additions to documentation
#15415
opened Aug 1, 2024 by
PhoenixIra
norm_num for Nat.factors
t-meta
Tactics, attributes or user commands
#15410
opened Aug 1, 2024 by
eric-wieser
The Shapley-Folkman lemma
good first issue
Good for newcomers
t-analysis
Analysis (normed *, calculus)
#14427
opened Jul 4, 2024 by
YaelDillies
clean up completely normal results to use Topological spaces, uniform spaces, metric spaces, filters
SeparatedNhds
t-topology
#14202
opened Jun 27, 2024 by
StevenClontz
duplicated definition of the pullback functor between over categories
#13998
opened Jun 20, 2024 by
emilyriehl
Tracking issue: try replacing Measure theory / Probability theory
tech debt
tracking cross-cutting technical debt
measurability
by fun_prop
t-measure-probability
#13864
opened Jun 15, 2024 by
grunweg
Data/Tree: Add New feature or request
good first issue
Good for newcomers
Traversable
instance.
enhancement
#13572
opened Jun 6, 2024 by
BoltonBailey
Rename Good for newcomers
please-adopt
zpow_le_zpow
and rpow_le_rpow
good first issue
#13544
opened Jun 5, 2024 by
BoltonBailey
notation3
doesn't support unparenthesized multiple binders like Π₀ i j, δ i j
t-meta
#13496
opened Jun 4, 2024 by
Komyyy
Regression after disabling
ConcreteCategory.instFunLike
as a global instance
#13342
opened May 29, 2024 by
dagurtomas
General geometric representations of a Coxeter group
#13291
opened May 27, 2024 by
trivial1711
1 of 9 tasks
Tracking: explicit universes can improve performance substantially
performance-hack
Something that improves performance but is poorly understood.
#12737
opened May 7, 2024 by
mattrobball
Porting note: Mathlib3 to Mathlib4 porting notes.
simp
doesn't apply simp
lemma unless parenthesized
porting-notes
#12717
opened May 6, 2024 by
Ruben-VandeVelde
tracking issue for
set_option backward.isDefEq.lazyProjDelta false
#12535
opened Apr 30, 2024 by
semorrison
tracking issue for
set_option backward.isDefEq.lazyWhnfCore false
#12534
opened Apr 30, 2024 by
semorrison
tracking issue for
set_option backward.synthInstance.canonInstances false
#12532
opened Apr 30, 2024 by
semorrison
Previous Next
ProTip!
Type g i on any issue or pull request to go back to the issue listing page.