{"action":"created","comment":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/comments/173767298","pull_request_review_id":103007574,"id":173767298,"diff_hunk":"@@ -0,0 +1,298 @@\n+/- \n+Copyright (c) 2018 Louis Carlin. All rights reserved.\n+Released under Apache 2.0 license as described in the file LICENSE.\n+Authors: Louis Carlin\n+\n+Euclidean domains and Euclidean algorithm (extended to come)\n+A lot is based on pre-existing code in mathlib for natural number gcds\n+-/\n+import tactic.ring\n+\n+universe u\n+\n+class euclidean_domain (α : Type u) extends integral_domain α :=\n+(quotient : α → α → α)\n+(remainder : α → α → α)\n+(quotient_mul_add_remainder_eq : ∀ a b, (quotient a b) * b + (remainder a b) = a) -- This could be changed to the same order as int.mod_add_div. We normally write qb+r rather than r + qb though.\n+(valuation : α → ℕ)\n+(valuation_remainder_lt : ∀ a b, b ≠ 0 → valuation (remainder a b) <  valuation b)\n+(le_valuation_mul : ∀ a b, b ≠ 0 → valuation a ≤ valuation (a*b))\n+(decidable_eq : ∀ a b : α, decidable (a=b))\n+/-\n+le_valuation_mul is often not a required in definitions of a euclidean domain since given the other properties we can show there is a (noncomputable) euclidean domain α with the property le_valuation_mul.\n+So potentially this definition could be split into two different ones (euclidean_domain_weak and euclidean_domain_strong) with a noncomputable function from weak to strong.\n+I've currently divided the lemmas into strong and weak depending on whether they require le_valuation_mul or not.\n+-/\n+\n+namespace euclidean_domain\n+variable {α : Type u}\n+variables [euclidean_domain α]\n+\n+instance (a b : α) : decidable (a = b) := decidable_eq a b\n+\n+instance : has_div α := ⟨quotient⟩\n+\n+instance : has_mod α := ⟨remainder⟩\n+\n+instance : has_sizeof α := ⟨valuation⟩\n+\n+lemma gcd_decreasing (a b : α) (w : a ≠ 0) : has_well_founded.r (b % a) a := valuation_remainder_lt b a w\n+\n+def gcd : α → α → α\n+| a b := if a_zero : a = 0 then b\n+     else have h : has_well_founded.r (b % a) a := gcd_decreasing a b a_zero,\n+        gcd (b%a) a\n+\n+/- weak lemmas -/\n+\n+@[simp] lemma mod_zero (a : α) : a % 0 = a :=\n+begin\n+  have := euclidean_domain.quotient_mul_add_remainder_eq a 0,\n+  simp at this,\n+  exact this,\n+end\n+\n+lemma dvd_mod_self (a : α) : a ∣ a % a :=\n+begin\n+  let d := (a/a)*a, -- ring tactic can't solve things without this\n+  have : a%a = a - (a/a)*a, from\n+    calc\n+      a%a = d + a%a  - d : by ring\n+      ... = (a/a)*a + a%a - (a/a)*a : by dsimp [d]; refl\n+      ... = a - (a/a)*a : by simp [(%), (/), quotient_mul_add_remainder_eq a a],\n+  rw this,\n+  exact dvd_sub (dvd_refl a) (dvd_mul_left a (a/a)),\n+end\n+\n+lemma mod_lt  : ∀ (a : α) {b : α}, valuation b > valuation (0:α) →  valuation (a%b) < valuation b :=\n+begin\n+  intros a b h,\n+  by_cases b_zero : (b=0),\n+  {\n+    rw b_zero at h,\n+    have := lt_irrefl (valuation (0:α)),\n+    contradiction,\n+  },\n+  {\n+    exact valuation_remainder_lt a b b_zero,\n+  }\n+end\n+\n+lemma neq_zero_lt_mod_lt (a b : α) :  b ≠ 0 → valuation (a%b) < valuation b\n+| hnb := valuation_remainder_lt a b hnb\n+\n+lemma dvd_mod {a b c : α} : c ∣ a → c ∣ b → c ∣ a % b :=\n+begin\n+  intros dvd_a dvd_b,\n+  have : remainder a b = a - quotient a b * b, from\n+  calc \n+    a%b = quotient a b * b + a%b - quotient a b * b : by ring\n+    ... = a - quotient a b * b : by {dsimp[(%)]; rw (quotient_mul_add_remainder_eq a b)},\n+  dsimp [(%)], \n+  rw this,\n+  exact dvd_sub dvd_a (dvd_mul_of_dvd_right dvd_b (a/b)),\n+end\n+\n+/- strong lemmas -/\n+\n+lemma val_lt_one (a : α) : valuation a < valuation (1:α) → a = 0 :=\n+begin\n+  intro a_lt,\n+  by_cases a = 0,\n+  { exact h},\n+  { \n+    have := le_valuation_mul (1:α) a h,\n+    simp at this,\n+    have := not_le_of_lt a_lt,\n+    contradiction\n+  }\n+end\n+\n+lemma val_dvd_le : ∀ a b : α, b ∣ a → a ≠ 0 → valuation b ≤ valuation a\n+| _ b ⟨d, rfl⟩ ha :=\n+begin\n+  by_cases d = 0,\n+  {\n+    simp[h] at ha,\n+    contradiction\n+  },\n+  {\n+    exact le_valuation_mul b d h,\n+  }\n+end\n+\n+@[simp] lemma mod_one (a : α) : a % 1 = 0 := \n+val_lt_one _ (valuation_remainder_lt a 1 one_ne_zero)\n+\n+@[simp] lemma zero_mod (b : α) : 0 % b = 0 :=\n+begin\n+  have h : remainder 0 b = b * (-quotient 0 b ), from\n+    calc\n+      remainder 0 b = quotient 0 b * b + remainder 0 b + b * (-quotient 0 b ) : by ring\n+      ...                       = b * (-quotient 0 b ) : by rw [quotient_mul_add_remainder_eq 0 b, zero_add],\n+  by_cases quotient_zero : (-quotient 0 b) = 0,\n+  {\n+    simp[quotient_zero] at h,\n+    exact h\n+  },\n+  {\n+    by_cases h'' : b = 0,\n+    {\n+      rw h'',\n+      simp\n+    },\n+    {\n+      have := not_le_of_lt (valuation_remainder_lt 0 b h''),\n+      rw h at this,\n+      have := le_valuation_mul b (-quotient 0 b) quotient_zero,\n+      contradiction,\n+    }\n+  }\n+end\n+\n+@[simp] lemma zero_div (b : α) (hnb : b ≠ 0) : 0 / b = 0 :=\n+begin\n+  have h1 : remainder 0 b = 0, from zero_mod b,\n+  have h2 := quotient_mul_add_remainder_eq 0 b,\n+  simp[h1] at h2,\n+  cases eq_zero_or_eq_zero_of_mul_eq_zero h2,\n+  { exact h },\n+  { contradiction }\n+end\n+\n+@[simp] lemma mod_self (a : α) : a % a = 0 :=\n+begin\n+  have := quotient_mul_add_remainder_eq a a,\n+  cases (dvd_mod_self a) with m a_mul,","path":"algebra/euclidean_domain.lean","position":164,"original_position":166,"commit_id":"9c6b68e5f2e7c383f11753bb01e4a5e31658d70c","original_commit_id":"9d6816ca85d21e683fbb28cb49f1c7d0524b3994","user":{"login":"kbuzzard","id":31867827,"avatar_url":"https://avatars3.githubusercontent.com/u/31867827?v=4","gravatar_id":"","url":"https://api.github.com/users/kbuzzard","html_url":"https://github.com/kbuzzard","followers_url":"https://api.github.com/users/kbuzzard/followers","following_url":"https://api.github.com/users/kbuzzard/following{/other_user}","gists_url":"https://api.github.com/users/kbuzzard/gists{/gist_id}","starred_url":"https://api.github.com/users/kbuzzard/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kbuzzard/subscriptions","organizations_url":"https://api.github.com/users/kbuzzard/orgs","repos_url":"https://api.github.com/users/kbuzzard/repos","events_url":"https://api.github.com/users/kbuzzard/events{/privacy}","received_events_url":"https://api.github.com/users/kbuzzard/received_events","type":"User","site_admin":false},"body":"Why not write the first part of the proof in term mode, and switch to tactic mode when the going gets tough? This still seems to compile:\r\n\r\n```\r\n@[simp] lemma mod_self (a : α) : a % a = 0 :=\r\nlet ⟨m, a_mul⟩ := dvd_mod_self a in begin\r\n  have := quotient_mul_add_remainder_eq a a,\r\n  by_cases m = 0,\r\n  {\r\n\r\n...\r\n```\r\n\r\nand indeed you even seem to be able to comment out the `have := quotient_mul_add_remainder_eq a a` line. \r\n\r\nI had a fear of writing proofs in term mode for a long time, but now I realise that actually for some stuff term mode is more natural than tactic mode. Tactic mode comes into its own when you're actually using tactics (e.g. `rw` is far less painful than all the `eq.subst` stuff that term mode would make you do) but sometimes term mode is more natural if you're not using too many tactics.","created_at":"2018-03-12T11:38:20Z","updated_at":"2018-03-12T11:38:20Z","html_url":"https://github.com/leanprover/mathlib/pull/78#discussion_r173767298","pull_request_url":"https://api.github.com/repos/leanprover/mathlib/pulls/78","author_association":"CONTRIBUTOR","_links":{"self":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/comments/173767298"},"html":{"href":"https://github.com/leanprover/mathlib/pull/78#discussion_r173767298"},"pull_request":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/78"}},"in_reply_to_id":173764877},"pull_request":{"url":"https://api.github.com/repos/leanprover/mathlib/pulls/78","id":174164549,"html_url":"https://github.com/leanprover/mathlib/pull/78","diff_url":"https://github.com/leanprover/mathlib/pull/78.diff","patch_url":"https://github.com/leanprover/mathlib/pull/78.patch","issue_url":"https://api.github.com/repos/leanprover/mathlib/issues/78","number":78,"state":"open","locked":false,"title":"[WIP] feat (euclidean domains / euclidean algorithm)","user":{"login":"louisanu","id":33954732,"avatar_url":"https://avatars2.githubusercontent.com/u/33954732?v=4","gravatar_id":"","url":"https://api.github.com/users/louisanu","html_url":"https://github.com/louisanu","followers_url":"https://api.github.com/users/louisanu/followers","following_url":"https://api.github.com/users/louisanu/following{/other_user}","gists_url":"https://api.github.com/users/louisanu/gists{/gist_id}","starred_url":"https://api.github.com/users/louisanu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/louisanu/subscriptions","organizations_url":"https://api.github.com/users/louisanu/orgs","repos_url":"https://api.github.com/users/louisanu/repos","events_url":"https://api.github.com/users/louisanu/events{/privacy}","received_events_url":"https://api.github.com/users/louisanu/received_events","type":"User","site_admin":false},"body":"I implemented Euclidean domains as well as the Euclidean algorithm, for the most part by writing generalised versions of things in the natural number gcd files.\r\nI also have a version of the extended Euclidean algorithm and some other bits and pieces but I thought I'd get some feedback on this first.\r\n\r\nI have a writeup (slightly out of date with the definition I ended up using) on some of the process/decisions here: https://tqft.net/web/research/students/LouisCarlin/EuclideanDomainsInLean.pdf","created_at":"2018-03-10T10:39:06Z","updated_at":"2018-03-12T11:38:20Z","closed_at":null,"merged_at":null,"merge_commit_sha":"2575ed7b0e3f46567a5722384e95a98a0bebbab9","assignee":null,"assignees":[],"requested_reviewers":[],"requested_teams":[],"labels":[],"milestone":null,"commits_url":"https://api.github.com/repos/leanprover/mathlib/pulls/78/commits","review_comments_url":"https://api.github.com/repos/leanprover/mathlib/pulls/78/comments","review_comment_url":"https://api.github.com/repos/leanprover/mathlib/pulls/comments{/number}","comments_url":"https://api.github.com/repos/leanprover/mathlib/issues/78/comments","statuses_url":"https://api.github.com/repos/leanprover/mathlib/statuses/9c6b68e5f2e7c383f11753bb01e4a5e31658d70c","head":{"label":"louisanu:euclidean_domain","ref":"euclidean_domain","sha":"9c6b68e5f2e7c383f11753bb01e4a5e31658d70c","user":{"login":"louisanu","id":33954732,"avatar_url":"https://avatars2.githubusercontent.com/u/33954732?v=4","gravatar_id":"","url":"https://api.github.com/users/louisanu","html_url":"https://github.com/louisanu","followers_url":"https://api.github.com/users/louisanu/followers","following_url":"https://api.github.com/users/louisanu/following{/other_user}","gists_url":"https://api.github.com/users/louisanu/gists{/gist_id}","starred_url":"https://api.github.com/users/louisanu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/louisanu/subscriptions","organizations_url":"https://api.github.com/users/louisanu/orgs","repos_url":"https://api.github.com/users/louisanu/repos","events_url":"https://api.github.com/users/louisanu/events{/privacy}","received_events_url":"https://api.github.com/users/louisanu/received_events","type":"User","site_admin":false},"repo":{"id":124519997,"name":"mathlib","full_name":"louisanu/mathlib","owner":{"login":"louisanu","id":33954732,"avatar_url":"https://avatars2.githubusercontent.com/u/33954732?v=4","gravatar_id":"","url":"https://api.github.com/users/louisanu","html_url":"https://github.com/louisanu","followers_url":"https://api.github.com/users/louisanu/followers","following_url":"https://api.github.com/users/louisanu/following{/other_user}","gists_url":"https://api.github.com/users/louisanu/gists{/gist_id}","starred_url":"https://api.github.com/users/louisanu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/louisanu/subscriptions","organizations_url":"https://api.github.com/users/louisanu/orgs","repos_url":"https://api.github.com/users/louisanu/repos","events_url":"https://api.github.com/users/louisanu/events{/privacy}","received_events_url":"https://api.github.com/users/louisanu/received_events","type":"User","site_admin":false},"private":false,"html_url":"https://github.com/louisanu/mathlib","description":"Lean mathematical components library","fork":true,"url":"https://api.github.com/repos/louisanu/mathlib","forks_url":"https://api.github.com/repos/louisanu/mathlib/forks","keys_url":"https://api.github.com/repos/louisanu/mathlib/keys{/key_id}","collaborators_url":"https://api.github.com/repos/louisanu/mathlib/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/louisanu/mathlib/teams","hooks_url":"https://api.github.com/repos/louisanu/mathlib/hooks","issue_events_url":"https://api.github.com/repos/louisanu/mathlib/issues/events{/number}","events_url":"https://api.github.com/repos/louisanu/mathlib/events","assignees_url":"https://api.github.com/repos/louisanu/mathlib/assignees{/user}","branches_url":"https://api.github.com/repos/louisanu/mathlib/branches{/branch}","tags_url":"https://api.github.com/repos/louisanu/mathlib/tags","blobs_url":"https://api.github.com/repos/louisanu/mathlib/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/louisanu/mathlib/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/louisanu/mathlib/git/refs{/sha}","trees_url":"https://api.github.com/repos/louisanu/mathlib/git/trees{/sha}","statuses_url":"https://api.github.com/repos/louisanu/mathlib/statuses/{sha}","languages_url":"https://api.github.com/repos/louisanu/mathlib/languages","stargazers_url":"https://api.github.com/repos/louisanu/mathlib/stargazers","contributors_url":"https://api.github.com/repos/louisanu/mathlib/contributors","subscribers_url":"https://api.github.com/repos/louisanu/mathlib/subscribers","subscription_url":"https://api.github.com/repos/louisanu/mathlib/subscription","commits_url":"https://api.github.com/repos/louisanu/mathlib/commits{/sha}","git_commits_url":"https://api.github.com/repos/louisanu/mathlib/git/commits{/sha}","comments_url":"https://api.github.com/repos/louisanu/mathlib/comments{/number}","issue_comment_url":"https://api.github.com/repos/louisanu/mathlib/issues/comments{/number}","contents_url":"https://api.github.com/repos/louisanu/mathlib/contents/{+path}","compare_url":"https://api.github.com/repos/louisanu/mathlib/compare/{base}...{head}","merges_url":"https://api.github.com/repos/louisanu/mathlib/merges","archive_url":"https://api.github.com/repos/louisanu/mathlib/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/louisanu/mathlib/downloads","issues_url":"https://api.github.com/repos/louisanu/mathlib/issues{/number}","pulls_url":"https://api.github.com/repos/louisanu/mathlib/pulls{/number}","milestones_url":"https://api.github.com/repos/louisanu/mathlib/milestones{/number}","notifications_url":"https://api.github.com/repos/louisanu/mathlib/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/louisanu/mathlib/labels{/name}","releases_url":"https://api.github.com/repos/louisanu/mathlib/releases{/id}","deployments_url":"https://api.github.com/repos/louisanu/mathlib/deployments","created_at":"2018-03-09T09:38:03Z","updated_at":"2018-03-09T09:38:05Z","pushed_at":"2018-03-12T11:05:50Z","git_url":"git://github.com/louisanu/mathlib.git","ssh_url":"git@github.com:louisanu/mathlib.git","clone_url":"https://github.com/louisanu/mathlib.git","svn_url":"https://github.com/louisanu/mathlib","homepage":"","size":2124,"stargazers_count":0,"watchers_count":0,"language":"Lean","has_issues":false,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":0,"mirror_url":null,"archived":false,"open_issues_count":0,"license":{"key":"apache-2.0","name":"Apache License 2.0","spdx_id":"Apache-2.0","url":"https://api.github.com/licenses/apache-2.0"},"forks":0,"open_issues":0,"watchers":0,"default_branch":"master"}},"base":{"label":"leanprover:master","ref":"master","sha":"d78c8ea201ddf8da3f4356a63f65332a8037c3a6","user":{"login":"leanprover","id":7233018,"avatar_url":"https://avatars3.githubusercontent.com/u/7233018?v=4","gravatar_id":"","url":"https://api.github.com/users/leanprover","html_url":"https://github.com/leanprover","followers_url":"https://api.github.com/users/leanprover/followers","following_url":"https://api.github.com/users/leanprover/following{/other_user}","gists_url":"https://api.github.com/users/leanprover/gists{/gist_id}","starred_url":"https://api.github.com/users/leanprover/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leanprover/subscriptions","organizations_url":"https://api.github.com/users/leanprover/orgs","repos_url":"https://api.github.com/users/leanprover/repos","events_url":"https://api.github.com/users/leanprover/events{/privacy}","received_events_url":"https://api.github.com/users/leanprover/received_events","type":"Organization","site_admin":false},"repo":{"id":97922418,"name":"mathlib","full_name":"leanprover/mathlib","owner":{"login":"leanprover","id":7233018,"avatar_url":"https://avatars3.githubusercontent.com/u/7233018?v=4","gravatar_id":"","url":"https://api.github.com/users/leanprover","html_url":"https://github.com/leanprover","followers_url":"https://api.github.com/users/leanprover/followers","following_url":"https://api.github.com/users/leanprover/following{/other_user}","gists_url":"https://api.github.com/users/leanprover/gists{/gist_id}","starred_url":"https://api.github.com/users/leanprover/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leanprover/subscriptions","organizations_url":"https://api.github.com/users/leanprover/orgs","repos_url":"https://api.github.com/users/leanprover/repos","events_url":"https://api.github.com/users/leanprover/events{/privacy}","received_events_url":"https://api.github.com/users/leanprover/received_events","type":"Organization","site_admin":false},"private":false,"html_url":"https://github.com/leanprover/mathlib","description":"Lean mathematical components library","fork":false,"url":"https://api.github.com/repos/leanprover/mathlib","forks_url":"https://api.github.com/repos/leanprover/mathlib/forks","keys_url":"https://api.github.com/repos/leanprover/mathlib/keys{/key_id}","collaborators_url":"https://api.github.com/repos/leanprover/mathlib/collaborators{/collaborator}","teams_url":"https://api.github.com/repos/leanprover/mathlib/teams","hooks_url":"https://api.github.com/repos/leanprover/mathlib/hooks","issue_events_url":"https://api.github.com/repos/leanprover/mathlib/issues/events{/number}","events_url":"https://api.github.com/repos/leanprover/mathlib/events","assignees_url":"https://api.github.com/repos/leanprover/mathlib/assignees{/user}","branches_url":"https://api.github.com/repos/leanprover/mathlib/branches{/branch}","tags_url":"https://api.github.com/repos/leanprover/mathlib/tags","blobs_url":"https://api.github.com/repos/leanprover/mathlib/git/blobs{/sha}","git_tags_url":"https://api.github.com/repos/leanprover/mathlib/git/tags{/sha}","git_refs_url":"https://api.github.com/repos/leanprover/mathlib/git/refs{/sha}","trees_url":"https://api.github.com/repos/leanprover/mathlib/git/trees{/sha}","statuses_url":"https://api.github.com/repos/leanprover/mathlib/statuses/{sha}","languages_url":"https://api.github.com/repos/leanprover/mathlib/languages","stargazers_url":"https://api.github.com/repos/leanprover/mathlib/stargazers","contributors_url":"https://api.github.com/repos/leanprover/mathlib/contributors","subscribers_url":"https://api.github.com/repos/leanprover/mathlib/subscribers","subscription_url":"https://api.github.com/repos/leanprover/mathlib/subscription","commits_url":"https://api.github.com/repos/leanprover/mathlib/commits{/sha}","git_commits_url":"https://api.github.com/repos/leanprover/mathlib/git/commits{/sha}","comments_url":"https://api.github.com/repos/leanprover/mathlib/comments{/number}","issue_comment_url":"https://api.github.com/repos/leanprover/mathlib/issues/comments{/number}","contents_url":"https://api.github.com/repos/leanprover/mathlib/contents/{+path}","compare_url":"https://api.github.com/repos/leanprover/mathlib/compare/{base}...{head}","merges_url":"https://api.github.com/repos/leanprover/mathlib/merges","archive_url":"https://api.github.com/repos/leanprover/mathlib/{archive_format}{/ref}","downloads_url":"https://api.github.com/repos/leanprover/mathlib/downloads","issues_url":"https://api.github.com/repos/leanprover/mathlib/issues{/number}","pulls_url":"https://api.github.com/repos/leanprover/mathlib/pulls{/number}","milestones_url":"https://api.github.com/repos/leanprover/mathlib/milestones{/number}","notifications_url":"https://api.github.com/repos/leanprover/mathlib/notifications{?since,all,participating}","labels_url":"https://api.github.com/repos/leanprover/mathlib/labels{/name}","releases_url":"https://api.github.com/repos/leanprover/mathlib/releases{/id}","deployments_url":"https://api.github.com/repos/leanprover/mathlib/deployments","created_at":"2017-07-21T08:02:10Z","updated_at":"2018-02-19T15:12:06Z","pushed_at":"2018-03-12T11:05:51Z","git_url":"git://github.com/leanprover/mathlib.git","ssh_url":"git@github.com:leanprover/mathlib.git","clone_url":"https://github.com/leanprover/mathlib.git","svn_url":"https://github.com/leanprover/mathlib","homepage":"","size":2171,"stargazers_count":20,"watchers_count":20,"language":"Lean","has_issues":true,"has_projects":true,"has_downloads":true,"has_wiki":true,"has_pages":false,"forks_count":18,"mirror_url":null,"archived":false,"open_issues_count":11,"license":{"key":"apache-2.0","name":"Apache License 2.0","spdx_id":"Apache-2.0","url":"https://api.github.com/licenses/apache-2.0"},"forks":18,"open_issues":11,"watchers":20,"default_branch":"master"}},"_links":{"self":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/78"},"html":{"href":"https://github.com/leanprover/mathlib/pull/78"},"issue":{"href":"https://api.github.com/repos/leanprover/mathlib/issues/78"},"comments":{"href":"https://api.github.com/repos/leanprover/mathlib/issues/78/comments"},"review_comments":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/78/comments"},"review_comment":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/comments{/number}"},"commits":{"href":"https://api.github.com/repos/leanprover/mathlib/pulls/78/commits"},"statuses":{"href":"https://api.github.com/repos/leanprover/mathlib/statuses/9c6b68e5f2e7c383f11753bb01e4a5e31658d70c"}},"author_association":"NONE"}}
{"actor":{"display_login":"kbuzzard"}}