issues
search
leanprover-community
/
mathlib3
Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k
stars
299
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
old WIP trying to replace fractional_ideal by submodule in class_group: to be ported
#19245
alreadydone
closed
2 months ago
0
refactor: Remove the K argument from exp
#19244
eric-wieser
closed
10 months ago
1
[Merged by Bors] - doc: Add a warning mentioning Lean 4 to the readme
#19243
eric-wieser
closed
11 months ago
2
chore(LinearAlgebra/DirectSum/TensorProduct): missing lemma
#19242
eric-wieser
closed
11 months ago
0
chore(*): add mathlib4 synchronization comments
#19240
github-actions[bot]
opened
1 year ago
0
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19239
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19238
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - fix: handle archive and counterexamples correctly when adding port comments
#19237
eric-wieser
closed
1 year ago
2
[Merged by Bors] - feat(linear_algebra/orientation): add `orientation.reindex`
#19236
eric-wieser
closed
1 year ago
2
[Merged by Bors] - feat(*/prod): `prod_prod_prod` equivs
#19235
eric-wieser
closed
1 year ago
4
[Merged by Bors] - chore(ring_theory/kaehler): cleanup instances
#19234
eric-wieser
closed
1 year ago
2
[Merged by Bors] - fix(tactic/linarith): instantiate metavariables in linarith
#19233
eric-wieser
closed
1 year ago
2
[Merged by Bors] - fix(tactic/interval_cases): instantiate metavars
#19232
eric-wieser
closed
1 year ago
5
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19231
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(topology/sheaves): revert universe generalizations from #19153
#19230
semorrison
closed
1 year ago
4
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19229
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - fix(control/traversable/derive): the `functor` deriving handler makes weird definitions for inductive types which have recursive arguments separated by a non-recursive argument
#19228
Komyyy
closed
1 year ago
2
[Merged by Bors] - chore(scripts): update nolints.txt
#19227
leanprover-community-bot
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19226
github-actions[bot]
closed
1 year ago
2
refactor: change notation for interval integrals
#19225
urkud
closed
2 months ago
2
feat(topology/order): Add closure.mono
#19224
mans0954
closed
1 year ago
4
[Merged by Bors] - refactor(*): move all `mk_simp_attribute` commands to 1 file
#19223
urkud
closed
1 year ago
4
[Merged by Bors] - chore(category_theory/concrete_category): reorder universes
#19222
semorrison
closed
1 year ago
2
[Merged by Bors] - refactor: redefine `bundle.total_space`
#19221
urkud
closed
1 year ago
6
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19220
github-actions[bot]
closed
1 year ago
2
feat(topology/algebra/infinite_sum) : define infinite products
#19219
AntoineChambert-Loir
opened
1 year ago
1
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19218
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(category_theory/limits/construction/over): rename default to basic
#19217
semorrison
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19216
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19215
github-actions[bot]
closed
1 year ago
3
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19214
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19213
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(analysis/complex/upper_half_plane,number_theory/modular_forms): reduce dependency on manifolds
#19212
urkud
closed
1 year ago
3
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19211
github-actions[bot]
closed
1 year ago
2
feat(topology/algebra/module/alternating): new file
#19210
urkud
closed
1 year ago
2
[Merged by Bors] - feat(manifold/{cont_mdiff,algebra/smooth_functions}): restriction as a homomorphism between spaces of smooth functions
#19209
hrmacbeth
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19208
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19207
github-actions[bot]
closed
1 year ago
2
feat(combinatorics/simple_graph): Triangle counting
#19206
YaelDillies
closed
9 months ago
1
make it a def
#19205
riccardobrasca
closed
1 year ago
1
[Merged by Bors] - refactor(data/matrix/invertible): more results about invertible matrices
#19204
eric-wieser
closed
1 year ago
8
[Merged by Bors] - feat(combinatorics/simple_graph): More clique lemmas
#19203
YaelDillies
closed
10 months ago
1
feat(combinatorics/simple_graph): Construct a tripartite graph from its triangles
#19202
YaelDillies
closed
9 months ago
2
feat(combinatorics/simple_graph): Locally linear graphs
#19201
YaelDillies
closed
9 months ago
2
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19200
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - feat(measure_theory/integral/average): Lebesgue average
#19199
YaelDillies
closed
1 year ago
1
[Merged by Bors] - feat(set_theory/cardinal/finite): prove lemmas to handle part_enat.card
#19198
AntoineChambert-Loir
closed
1 year ago
2
[Merged by Bors] - chore(data/zmod/algebra): make zmod.algebra a def
#19197
riccardobrasca
closed
1 year ago
3
[Merged by Bors] - chore(*): add mathlib4 synchronization comments
#19196
github-actions[bot]
closed
1 year ago
2
[Merged by Bors] - style(archive.100-theorems-list.xx_theorem_name): rename to `wiedijk_100_theorems.theorem_name`
#19195
Komyyy
closed
1 year ago
5
Next