Commit 2025-02-17 12:13 fa01e96e

View on Github →

feat: finset of pairs of divisors of an integer (#21912) Compute the antidiagonal of divisors of an integer z, namely the finset of pairs (a, b) : ℤ × ℤ such that a * b = n (unless z = 0, in which case we set the finset to be empty by convention).

Estimated changes

Modified Mathlib/Data/Nat/Cast/Order/Ring.lean

modified theorem Nat.abs_cast

modified theorem Nat.abs_ofNat

added theorem Nat.cast_eq_neg_cast

added theorem Nat.neg_cast_eq_cast

Modified Mathlib/NumberTheory/Divisors.lean

added def Int.divisorsAntidiag

added theorem Int.divisorsAntidiag_natCast

added theorem Int.divisorsAntidiag_neg

added theorem Int.divisorsAntidiag_neg_natCast

added theorem Int.divisorsAntidiag_ofNat

added theorem Int.divisorsAntidiag_zero

added theorem Int.map_neg_divisorsAntidiag

added theorem Int.map_prodComm_divisorsAntidiag

added theorem Int.mem_divisorsAntidiag

added theorem Int.neg_mem_divisorsAntidiag

added theorem Int.prodMk_mem_divisorsAntidiag

added theorem Int.swap_mem_divisorsAntidiag

added theorem Nat.prodMk_mem_divisorsAntidiag