Ecosyste.ms: Issues
An open API service for providing issue and pull request metadata for open source projects.
GitHub / leanprover-community/mathlib issues and pull requests
#61 - feat(data/real): cauchy sequence limit lemmas
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 9 comments
#61 - feat(data/real): cauchy sequence limit lemmas
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 9 comments
#60 - [WIP] Categories, unbundled
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 2 comments
#60 - [WIP] Categories, unbundled
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 2 comments
#60 - [WIP] Categories, unbundled
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 2 comments
#59 - [WIP] real cauchy sequence limits
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#59 - [WIP] real cauchy sequence limits
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#59 - [WIP] real cauchy sequence limits
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#58 - Docs
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
#58 - Docs
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
#57 - Equivalence of Cauchy sequences
Issue -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 3 comments
#56 - rcases and nested patterns
Issue -
State: closed - Opened by spl almost 7 years ago
#56 - rcases and nested patterns
Issue -
State: closed - Opened by spl almost 7 years ago
#56 - rcases and nested patterns
Issue -
State: closed - Opened by spl almost 7 years ago
#55 - feat(data/multiset): disjoint_union theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 8 comments
#54 - feat(data/multiset): disjoint_ndinsert theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 2 comments
#54 - feat(data/multiset): disjoint_ndinsert theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 2 comments
#54 - feat(data/multiset): disjoint_ndinsert theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 2 comments
#53 - feat (algebra/group_power) add pow_inv and pow_abs
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 4 comments
#53 - feat (algebra/group_power) add pow_inv and pow_abs
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 4 comments
#53 - feat (algebra/group_power) add pow_inv and pow_abs
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 4 comments
#52 - feat(data/equiv): generalize list_equiv_of_equiv over universes
Pull Request -
State: closed - Opened by spl almost 7 years ago
#52 - feat(data/equiv): generalize list_equiv_of_equiv over universes
Pull Request -
State: closed - Opened by spl almost 7 years ago
#51 - feat(data/list) update_nth_eq_nil, append_eq_nil
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 4 comments
#51 - feat(data/list) update_nth_eq_nil, append_eq_nil
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 4 comments
#50 - feat(algebra/archimedean): pow_unbounded_of_gt_one
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#50 - feat(algebra/archimedean): pow_unbounded_of_gt_one
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#50 - feat(algebra/archimedean): pow_unbounded_of_gt_one
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#49 - Update archimedean.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#49 - Update archimedean.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#49 - Update archimedean.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#48 - Create choose.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 6 comments
#48 - Create choose.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 6 comments
#48 - Create choose.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 6 comments
#47 - feat(order/basic) more max lemmas
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 5 comments
#47 - feat(order/basic) more max lemmas
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 5 comments
#47 - feat(order/basic) more max lemmas
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 5 comments
#46 - feat(analysis/metric_space) tends_iff_dist_tendsto_zero
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 4 comments
#46 - feat(analysis/metric_space) tends_iff_dist_tendsto_zero
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 4 comments
#46 - feat(analysis/metric_space) tends_iff_dist_tendsto_zero
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 4 comments
#45 - [WIP] initial commit, just the definition of categories, functors, and natural transformations
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 13 comments
#45 - [WIP] initial commit, just the definition of categories, functors, and natural transformations
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 13 comments
#45 - [WIP] initial commit, just the definition of categories, functors, and natural transformations
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 13 comments
#44 - feat(data/finset): not_mem theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 1 comment
#44 - feat(data/finset): not_mem theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 1 comment
#44 - feat(data/finset): not_mem theorems
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 1 comment
#43 - Create series.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#43 - Create series.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#43 - Create series.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#42 - Create limits.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#42 - Create limits.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#42 - Create limits.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#41 - Create exponential.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#41 - Create exponential.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#41 - Create exponential.lean
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
#40 - Definition of the ring of adeles of a number field
Issue -
State: closed - Opened by kbuzzard almost 7 years ago
- 1 comment
Labels: RFC
#40 - Definition of the ring of adeles of a number field
Issue -
State: closed - Opened by kbuzzard almost 7 years ago
- 1 comment
Labels: RFC
#40 - Definition of the ring of adeles of a number field
Issue -
State: closed - Opened by kbuzzard almost 7 years ago
- 1 comment
Labels: RFC
#39 - Update localization
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#39 - Update localization
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#39 - Update localization
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#38 - Create localization.lean
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
#38 - Create localization.lean
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
#38 - Create localization.lean
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
#37 - [WIP] Commutative algebra
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#37 - [WIP] Commutative algebra
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#37 - [WIP] Commutative algebra
Pull Request -
State: closed - Opened by kckennylau almost 7 years ago
- 2 comments
#36 - Conditionally complete lattices
Pull Request -
State: closed - Opened by sgouezel almost 7 years ago
- 3 comments
#36 - Conditionally complete lattices
Pull Request -
State: closed - Opened by sgouezel almost 7 years ago
- 3 comments
#36 - Conditionally complete lattices
Pull Request -
State: closed - Opened by sgouezel almost 7 years ago
- 3 comments
#35 - tendsto_dist nerfed
Issue -
State: closed - Opened by PatrickMassot almost 7 years ago
- 1 comment
#35 - tendsto_dist nerfed
Issue -
State: closed - Opened by PatrickMassot almost 7 years ago
- 1 comment
#34 - Added unfinished lemma and corrected a lemma
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#34 - Added unfinished lemma and corrected a lemma
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#34 - Added unfinished lemma and corrected a lemma
Pull Request -
State: closed - Opened by ChrisHughes24 almost 7 years ago
- 1 comment
#33 - Permutation group instance for any type
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
#33 - Permutation group instance for any type
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
#33 - Permutation group instance for any type
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
#32 - fixes for latest breaking changes in Lean; data/seq/wseq.lean is stil…
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 1 comment
#32 - fixes for latest breaking changes in Lean; data/seq/wseq.lean is stil…
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
- 1 comment
#31 - temporary fixes, turning off smart_unfolding in places
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
#31 - temporary fixes, turning off smart_unfolding in places
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
#31 - temporary fixes, turning off smart_unfolding in places
Pull Request -
State: closed - Opened by semorrison almost 7 years ago
#30 - Group morphisms
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 11 comments
#30 - Group morphisms
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 11 comments
#30 - Group morphisms
Pull Request -
State: closed - Opened by PatrickMassot almost 7 years ago
- 11 comments
#29 - feat(data/fin): fin.succ.inj
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 1 comment
#29 - feat(data/fin): fin.succ.inj
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 1 comment
#28 - feat(.travis.yml): export and run leanchecker
Pull Request -
State: closed - Opened by gebner almost 7 years ago
- 2 comments
#28 - feat(.travis.yml): export and run leanchecker
Pull Request -
State: closed - Opened by gebner almost 7 years ago
- 2 comments
#27 - Name clashes
Pull Request -
State: closed - Opened by gebner almost 7 years ago
- 6 comments
#27 - Name clashes
Pull Request -
State: closed - Opened by gebner almost 7 years ago
- 6 comments
#27 - Name clashes
Pull Request -
State: closed - Opened by gebner almost 7 years ago
- 6 comments
#26 - Definition of a scheme
Issue -
State: closed - Opened by kbuzzard almost 7 years ago
- 10 comments
Labels: RFC
#26 - Definition of a scheme
Issue -
State: closed - Opened by kbuzzard almost 7 years ago
- 10 comments
Labels: RFC
#25 - chore(.): adapt to change bc89ebc19c93392419b7bab8b68271db12855dc5 (improve how induction hypotheses are named)
Pull Request -
State: closed - Opened by spl almost 7 years ago
- 2 comments
#24 - theories/number_theory/pell.lean: unsolved goals
Issue -
State: closed - Opened by spl almost 7 years ago
- 4 comments
#24 - theories/number_theory/pell.lean: unsolved goals
Issue -
State: closed - Opened by spl almost 7 years ago
- 4 comments
#23 - fix(data/sigma): use Sort for psigma
Pull Request -
State: closed - Opened by spl almost 7 years ago
#23 - fix(data/sigma): use Sort for psigma
Pull Request -
State: closed - Opened by spl almost 7 years ago