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

#100 - feat(algebra/big_operators): update prod_bij_ne_one

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago - 1 comment

#99 - Adding some notes on calc

Pull Request - State: closed - Opened by kbuzzard over 6 years ago

#98 - fix(.travis.yml): fix some elan

Pull Request - State: closed - Opened by Kha over 6 years ago - 3 comments

#97 - chore(.travis.yml): show some elan

Pull Request - State: closed - Opened by Kha over 6 years ago - 2 comments

#97 - chore(.travis.yml): show some elan

Pull Request - State: closed - Opened by Kha over 6 years ago - 2 comments

#97 - chore(.travis.yml): show some elan

Pull Request - State: closed - Opened by Kha over 6 years ago - 2 comments

#96 - [WIP] Structures and classes tips and tricks

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 4 comments
Labels: WIP

#96 - [WIP] Structures and classes tips and tricks

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 4 comments
Labels: WIP

#96 - [WIP] Structures and classes tips and tricks

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 4 comments
Labels: WIP

#95 - feat(docs/styles): Some more indentation guidelines

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago

#95 - feat(docs/styles): Some more indentation guidelines

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago

#95 - feat(docs/styles): Some more indentation guidelines

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago

#94 - [WIP] subgroups and homomorphisms

Pull Request - State: closed - Opened by semorrison over 6 years ago - 4 comments

#94 - [WIP] subgroups and homomorphisms

Pull Request - State: closed - Opened by semorrison over 6 years ago - 4 comments

#94 - [WIP] subgroups and homomorphisms

Pull Request - State: closed - Opened by semorrison over 6 years ago - 4 comments

#93 - feat (data/int/modeq) Create modeq.lean

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#93 - feat (data/int/modeq) Create modeq.lean

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#93 - feat (data/int/modeq) Create modeq.lean

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#92 - Create free_group.lean

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 1 comment

#92 - Create free_group.lean

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 1 comment

#92 - Create free_group.lean

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 1 comment

#91 - Add nat.div_le_div : n ≤ m → n/k ≤ m/k

Pull Request - State: closed - Opened by MonoidMusician over 6 years ago - 2 comments

#90 - feat (data/nat/prime) lemmas about nat.factors

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#90 - feat (data/nat/prime) lemmas about nat.factors

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#90 - feat (data/nat/prime) lemmas about nat.factors

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#89 - Free groups

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 14 comments

#89 - Free groups

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 14 comments

#89 - Free groups

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 14 comments

#88 - Create Knaster_Tarski.lean

Pull Request - State: closed - Opened by kckennylau over 6 years ago - 3 comments

#87 - Probelm in analysis.real

Issue - State: closed - Opened by adhalanay over 6 years ago - 12 comments

#87 - Probelm in analysis.real

Issue - State: closed - Opened by adhalanay over 6 years ago - 12 comments

#87 - Probelm in analysis.real

Issue - State: closed - Opened by adhalanay over 6 years ago - 12 comments

#86 - fix(test suite): remove `sorry` warning in test suite

Pull Request - State: closed - Opened by cipher1024 over 6 years ago

#86 - fix(test suite): remove `sorry` warning in test suite

Pull Request - State: closed - Opened by cipher1024 over 6 years ago

#86 - fix(test suite): remove `sorry` warning in test suite

Pull Request - State: closed - Opened by cipher1024 over 6 years ago

#85 - Monotonicity

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 14 comments

#85 - Monotonicity

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 14 comments

#85 - Monotonicity

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 14 comments

#84 - `ring` tactic fails on some inputs

Issue - State: closed - Opened by digama0 over 6 years ago
Labels: bug

#84 - `ring` tactic fails on some inputs

Issue - State: closed - Opened by digama0 over 6 years ago
Labels: bug

#84 - `ring` tactic fails on some inputs

Issue - State: closed - Opened by digama0 over 6 years ago
Labels: bug

#83 - [WIP] feat (data/nat/choose) add card_subsets_eq_choose

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#83 - [WIP] feat (data/nat/choose) add card_subsets_eq_choose

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#83 - [WIP] feat (data/nat/choose) add card_subsets_eq_choose

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#82 - Docs simp notes

Pull Request - State: closed - Opened by kbuzzard over 6 years ago

#82 - Docs simp notes

Pull Request - State: closed - Opened by kbuzzard over 6 years ago

#82 - Docs simp notes

Pull Request - State: closed - Opened by kbuzzard over 6 years ago

#81 - Simp docs2

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#81 - Simp docs2

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#81 - Simp docs2

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#80 - Simp docs

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#80 - Simp docs

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#80 - Simp docs

Pull Request - State: closed - Opened by kbuzzard over 6 years ago - 1 comment

#79 - adding explanation of "change"

Pull Request - State: closed - Opened by kbuzzard over 6 years ago

#78 - feat (euclidean domains / euclidean algorithm)

Pull Request - State: closed - Opened by louisanu over 6 years ago - 18 comments

#77 - fix(analysis/topology/topological_structures)

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#77 - fix(analysis/topology/topological_structures)

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#77 - fix(analysis/topology/topological_structures)

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#76 - [WIP] `traversable` type class

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 28 comments
Labels: WIP

#76 - [WIP] `traversable` type class

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 28 comments
Labels: WIP

#76 - [WIP] `traversable` type class

Pull Request - State: closed - Opened by cipher1024 over 6 years ago - 28 comments
Labels: WIP

#75 - feat (docs/theories) update sets.md

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#75 - feat (docs/theories) update sets.md

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#75 - feat (docs/theories) update sets.md

Pull Request - State: closed - Opened by ChrisHughes24 over 6 years ago

#73 - feat(docs/extras/conv) Documents conv mode

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#73 - feat(docs/extras/conv) Documents conv mode

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#73 - feat(docs/extras/conv) Documents conv mode

Pull Request - State: closed - Opened by PatrickMassot over 6 years ago - 1 comment

#72 - changing bind to list.bind

Pull Request - State: closed - Opened by semorrison over 6 years ago - 1 comment

#72 - changing bind to list.bind

Pull Request - State: closed - Opened by semorrison over 6 years ago - 1 comment

#72 - changing bind to list.bind

Pull Request - State: closed - Opened by semorrison over 6 years ago - 1 comment

#71 - [WIP] added basic machinery for defining coinductive types

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 11 comments
Labels: WIP

#71 - [WIP] added basic machinery for defining coinductive types

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 11 comments
Labels: WIP

#71 - [WIP] added basic machinery for defining coinductive types

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 11 comments
Labels: WIP

#70 - fix(docs/tactics) update instance cache tactics doc

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago

#70 - fix(docs/tactics) update instance cache tactics doc

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago

#69 - feat(nightlies) adds a nightly lean working with mathlib

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 13 comments

#69 - feat(nightlies) adds a nightly lean working with mathlib

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 13 comments

#69 - feat(nightlies) adds a nightly lean working with mathlib

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 13 comments

#68 - feat(analysis/metric_space) adds squeeze theorem

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 2 comments

#68 - feat(analysis/metric_space) adds squeeze theorem

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 2 comments

#68 - feat(analysis/metric_space) adds squeeze theorem

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago - 2 comments

#67 - Document the find command

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago

#67 - Document the find command

Pull Request - State: closed - Opened by PatrickMassot almost 7 years ago

#66 - feat(data/finset): insert_union_distrib

Pull Request - State: closed - Opened by spl almost 7 years ago

#66 - feat(data/finset): insert_union_distrib

Pull Request - State: closed - Opened by spl almost 7 years ago

#66 - feat(data/finset): insert_union_distrib

Pull Request - State: closed - Opened by spl almost 7 years ago

#65 - feat(tactic): add `wlog` (without loss of generality), `tauto`, `auto…

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 31 comments

#65 - feat(tactic): add `wlog` (without loss of generality), `tauto`, `auto…

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 31 comments

#65 - feat(tactic): add `wlog` (without loss of generality), `tauto`, `auto…

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago - 31 comments

#64 - Wlog tactic

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago

#64 - Wlog tactic

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago

#64 - Wlog tactic

Pull Request - State: closed - Opened by cipher1024 almost 7 years ago

#63 - Remove unnecessary `finish` in `data.set.basic`

Pull Request - State: closed - Opened by kckennylau almost 7 years ago - 3 comments

#63 - Remove unnecessary `finish` in `data.set.basic`

Pull Request - State: closed - Opened by kckennylau almost 7 years ago - 3 comments

#63 - Remove unnecessary `finish` in `data.set.basic`

Pull Request - State: closed - Opened by kckennylau almost 7 years ago - 3 comments

#62 - feat(option.to_list)

Pull Request - State: closed - Opened by semorrison almost 7 years ago

#62 - feat(option.to_list)

Pull Request - State: closed - Opened by semorrison almost 7 years ago