{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/211","repository_url":"https://api.github.com/repos/leanprover/mathlib","labels_url":"https://api.github.com/repos/leanprover/mathlib/issues/211/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/211/comments","events_url":"https://api.github.com/repos/leanprover/mathlib/issues/211/events","html_url":"https://github.com/leanprover/mathlib/pull/211","id":343079564,"node_id":"MDExOlB1bGxSZXF1ZXN0MjAyODI3NTA1","number":211,"title":"feat(algebra/euclidean_domain) change definition of ED and instance for polynomials","user":{"login":"dorhinj","id":33847686,"node_id":"MDQ6VXNlcjMzODQ3Njg2","avatar_url":"https://avatars3.githubusercontent.com/u/33847686?v=4","gravatar_id":"","url":"https://api.github.com/users/dorhinj","html_url":"https://github.com/dorhinj","followers_url":"https://api.github.com/users/dorhinj/followers","following_url":"https://api.github.com/users/dorhinj/following{/other_user}","gists_url":"https://api.github.com/users/dorhinj/gists{/gist_id}","starred_url":"https://api.github.com/users/dorhinj/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dorhinj/subscriptions","organizations_url":"https://api.github.com/users/dorhinj/orgs","repos_url":"https://api.github.com/users/dorhinj/repos","events_url":"https://api.github.com/users/dorhinj/events{/privacy}","received_events_url":"https://api.github.com/users/dorhinj/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-07-20T11:53:34Z","updated_at":"2018-07-23T08:31:23Z","closed_at":null,"author_association":"CONTRIBUTOR","pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/211","html_url":"https://github.com/leanprover/mathlib/pull/211","diff_url":"https://github.com/leanprover/mathlib/pull/211.diff","patch_url":"https://github.com/leanprover/mathlib/pull/211.patch"},"body":"My suggestion for how to adapt the definition of Euclidean domain for polynomials. Euclidean domain now takes a well founded relation instead of a valuation.\r\n\r\nTO CONTRIBUTORS:\r\n\r\nMake sure you have:\r\n\r\n * [x] reviewed and applied the coding style: [coding](./docs/style.md), [naming](./docs/naming.md)\r\n * [x] for tactics:\r\n     * [x] added or adapted documentation in [tactics.md](./docs/tactics.md)\r\n     * [x] write an example of use of the new feature in [tactics.lean](./tests/tactics.lean)\r\n  * [x] make sure definitions and lemmas are put in the right files\r\n  * [x] make sure definitions and lemmas are not redundant\r\n\r\nFor reviewers: [code review check list](./docs/code-review.md)\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/mathlib/issues/comments/406981173","html_url":"https://github.com/leanprover/mathlib/pull/211#issuecomment-406981173","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/211","id":406981173,"node_id":"MDEyOklzc3VlQ29tbWVudDQwNjk4MTE3Mw==","user":{"login":"jcommelin","id":5636705,"node_id":"MDQ6VXNlcjU2MzY3MDU=","avatar_url":"https://avatars2.githubusercontent.com/u/5636705?v=4","gravatar_id":"","url":"https://api.github.com/users/jcommelin","html_url":"https://github.com/jcommelin","followers_url":"https://api.github.com/users/jcommelin/followers","following_url":"https://api.github.com/users/jcommelin/following{/other_user}","gists_url":"https://api.github.com/users/jcommelin/gists{/gist_id}","starred_url":"https://api.github.com/users/jcommelin/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jcommelin/subscriptions","organizations_url":"https://api.github.com/users/jcommelin/orgs","repos_url":"https://api.github.com/users/jcommelin/repos","events_url":"https://api.github.com/users/jcommelin/events{/privacy}","received_events_url":"https://api.github.com/users/jcommelin/received_events","type":"User","site_admin":false},"created_at":"2018-07-23T08:31:23Z","updated_at":"2018-07-23T08:31:23Z","author_association":"CONTRIBUTOR","body":"So, why don't we change the name to transfinite ED, and include a lemma that every ED is a transfinite ED. Type class inference should take care of the rest. The most important property (as far as I know) of an ED is that it is a PID."}}
{"actor":{"display_login":"jcommelin"}}