Commit 2026-05-01 13:07 dece6d67

View on Github →

refactor(NumberTheory): golf Mathlib/NumberTheory/Dioph (#38457)

  • golfs Mathlib/NumberTheory/Dioph by replacing the arithmetic proof in sub_dioph with grind
  • simplifies div_dioph by splitting on y = 0 ∨ 0 < y, then closing the positive case with Nat.div_eq_iff and grind Extracted from #38144 Open in Gitpod

Estimated changes

modified theorem Dioph.sub_dioph