Integer Divisors?

Stream: Is there code for X?

[Sabbir Rahman]

Is there something akin to Nat.divisors for Int? Generally if I know a dividies a constant, then using Nat.divisors I can easily limit a to cases. But I don't know how to do the same for Ints.

import Mathlib

example (a : ℕ) (h : a ∣ 10) : a = 1 ∨ a = 2 ∨ a = 5 ∨ a = 10 := by
  replace h : a ∈ Nat.divisors 10 := Nat.mem_divisors.mpr ⟨h, by norm_num⟩
  change a ∈ {1, 2, 5, 10} at h
  simpa using h

example (a : ℤ) (h : a ∣ 10) : a = 1 ∨ a = 2 ∨ a = 5 ∨ a = 10 ∨ a = -1 ∨ a = -2 ∨ a = -5 ∨ a = -10 := by
  sorry

If there isn't any Int divisors, what's the easy way to do the second example? I know one way is to use interval_cases but was hoping for something more elementary.

[Luigi Massacci]

@loogle Int, "Divisors"

[loogle]

:search: Lean.Grind.no_int_zero_divisors, Lean.Grind.instNoNatZeroDivisorsInt, and 37 more

[Luigi Massacci]

I guess you could use docs#Int.divisorsAntidiag

[Luigi Massacci]

Though whether you should I do not really know

[Sabbir Rahman]

I see that Int.divisorsAntidiag is made from Nat.divisorsAntidiag. Well to me it feels like similarly Int.divisors should've been made from Nat.divisors :/

[Sabbir Rahman]

The more I think about it, I feel like there should be Int.divisors. can I try to implement and create pr to add it? Not sure if there is any existing work for it though.

[Yaël Dillies]

@Paul Lezeau, I am losing track here, but don't we have Int.divisors somewhere?

[Arend Mellendijk]

There's docs#Int.divisorsAntidiag

[Arend Mellendijk]

Oops, I see Luigi already suggested that

[Niklas Halonen]

I happened to stumble on a similar question yesterday. This solution from formalising-mathematics-2024 might be useful

The key theorem used there is

theorem int_dvd_iff (x : ℤ) (n : ℤ) (hn : n ≠ 0) : x ∣ n ↔ x.natAbs ∈ n.natAbs.divisors := by
  simp [hn]

In my opinion this suffices and there is no need for Int.divisors, but maybe int_dvd_iff should be in mathlib (with a more suitable name like Int.dvd_iff_natAbs_mem_divisors).

[Sabbir Rahman]

The main usecase I see is that one should be able to jump form a ∣ 9797 to a ∈ {1, -1, 97, -97, 101, -101, 9797, -9797} easily. Because this is typically a trivial step in any proof. So int_dvd_iff trick is helpful, but still a bit boilerplate-y

[Paul Lezeau]

Yaël Dillies said:

Paul Lezeau, I am losing track here, but don't we have Int.divisors somewhere?

Hm I think I’ve never seen it before

[Sabbir Rahman]

in fact, even if Int.divisors is not created, following is also good I think

import Mathlib

theorem mythm (a b : ℤ) : a ∣ b ↔ a ∈ b.natAbs.divisors.map ⟨(↑), Nat.cast_injective⟩
    ∨ -a ∈ b.natAbs.divisors.map ⟨(↑), Nat.cast_injective⟩ := by sorry

example (a : ℤ) : a ∣ 123 ↔ a = 1 ∨ a = 3 ∨ a = 41 ∨ a = 123 ∨
    -a = 1 ∨ -a = 3 ∨ -a = 41 ∨ -a = 123 := by
  rw [mythm]
  repeat
    conv in Finset.map _ _ =>
      equals ({1, 3, 41, 123} : Finset ℤ) => decide
  simp
  tauto

[Eric Wieser]

I agree that we should define it

[Paul Lezeau]

Do you want to have a go at this @Sabbir Rahman ?

[Sabbir Rahman]

Yes, I'd love to. I assume the same file as Nat.divisors is ok, as it already contains both Nat and Int theorems for divisorsAntidiag

[Paul Lezeau]

Sounds good - feel free to ping me for a review;)

[Sabbir Rahman]

created PR 25209 to add int divisors :raised_hands:

[Yongshun Ye]

Hi I came across a case that needs these defs and theorems and thanks for all the work. One simple question on Int.divisorsAntidiag here: why is the name Int.divisorsAntidiag not consistent with Nat.divisorsAntidiagonal?

[Kevin Buzzard]

Probably just because mathlib grows organically and things sometimes get merged by people who miss little things. Probably a PR normalising conventions would be welcome!

[Yaël Dillies]

The plan here is to rename divisorsAntidiagonal to divisorsAntidiag. I was waiting on #21915 to be done before doing so, but I think it's not going to be ready anytime soon, so feel free to rename docs#Nat.divisorsAntidiagonal now!

[Eric Wieser]

What about docs#Finset.antidiagonal ?

[Weiyi Wang]

I understand naming is hard, but random abbreviation in mathlib still gets me sometimes

[Aaron Liu]

Yaël Dillies said:

The plan here is to rename divisorsAntidiagonal to divisorsAntidiag. I was waiting on #21915 to be done before doing so, but I think it's not going to be ready anytime soon, so feel free to rename docs#Nat.divisorsAntidiagonal now!

Why?

[Aaron Liu]

It's already hard enough finding stuff (it's divisors and proper divisors but when they're prime it becomes prime factors)

[Aaron Liu]

Do we need to introduce an abbreviation on top of that?

[Eric Wieser]

There's maybe an argument we should instead merge it with docs#Finset.HasMulAntidiagonal

[Aaron Liu]

Oh did we finally add mul antidiagonals?

[Eric Wieser]

We have docs#Finset.mulAntidiagonal but it's different

[Aaron Liu]

yet another way to spell everything

[Eric Wieser]

Either way, this points to the fact that antidiagonal is pretty established as a full name (for admittedly a bunch of related but different things) and we should match it for the time being

[Yaël Dillies]

I've started doing the renames to antidiag...

[Eric Wieser]

I would suggest not doing so without a Zulip poll (that is about every antidiagonal in mathlib, after listing all of them)