Commit 2026-05-10 14:42 f71cc9dd

View on Github →

chore(NumberTheory/Divisors): golf Int.mem_divisorsAntidiag (#38889) This PR merges the case split and removes duplicated proofs in Int.mem_divisorsAntidiag.

Estimated changes

Modified Mathlib/NumberTheory/Divisors.lean

modified theorem Int.mem_divisorsAntidiag