)]}'
{
  "commit": "7a2ef0b7a565fd8e9af5dc5613e2290ea6ce321c",
  "tree": "9a9d2dd3b77b1e8fb35f2887a814f3ce146ea4bb",
  "parents": [
    "a972c4f50dfc335559be8445c739e46d1df57b3a"
  ],
  "author": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sat Jan 31 13:17:48 2026 +1100"
  },
  "committer": {
    "name": "Kim Morrison",
    "email": "kim@tqft.net",
    "time": "Sat Jan 31 13:17:48 2026 +1100"
  },
  "message": "feat: add `Nat.ext_div_mod` and `Int.ext_ediv_emod`\n\nThis PR adds theorems that directly state that div and mod form an\ninjective pair: if `a / n \u003d b / n` and `a % n \u003d b % n` then `a \u003d b`.\nThese complement existing div/mod lemmas and are useful for extension\narguments.\n\nCo-Authored-By: Claude Opus 4.5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "83d3cdca5a75a89fa3c06d3b0c765d7d59f1dcf6",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Int/DivMod/Lemmas.lean",
      "new_id": "c3bdfebc54a36130976fe12d5d48d0d7f8fbb1cf",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Int/DivMod/Lemmas.lean"
    },
    {
      "type": "modify",
      "old_id": "1f9473d8cdbf1e0ba56206e38c9967ac30c25638",
      "old_mode": 33188,
      "old_path": "src/Init/Data/Nat/Div/Lemmas.lean",
      "new_id": "95b7553b9db8c4d7873993112ac02864d5c00583",
      "new_mode": 33188,
      "new_path": "src/Init/Data/Nat/Div/Lemmas.lean"
    }
  ]
}