Best module for contributing divisors lemma

Stream: mathlib4

[Adrian Marti]

Hi all, I'm fairly new to contributing to mathlib and I had a question!
I have this simple lemma about the set of divisors of a number being zero if and only if the number is zero.

/-- A number has infinitely many divisors if and only if it is zero. -/
lemma Nat.dvd_infinite (n : ℕ) : { m | m ∣ n }.Infinite ↔ n = 0 := by
  cases n
  case zero => simp [Set.infinite_univ]
  case succ n =>
    have h : {m : ℕ | m ∣ n + 1}.Finite :=
      Set.finite_iff_bddAbove.2 ⟨ _, fun m hm => Nat.le_of_dvd ( Nat.succ_pos _ ) hm ⟩
    simp [h]

I also have an integer version. I was wondering where the best place to put this in mathlib is. NumberTheory.Divisors, right along Nat.nonempty_divisors? Or is it better to put it somewhere in Data.Nat?

I also have an integer version for the lemma. I am also sure someone could come up with a way to golf the proof.