division and remainder as an equivalence

Stream: Is there code for X?

[Eric Wieser]

Do we have anything like this anywhere?

/-- The equivalence between `a` and `(a / n, a % n)` for nonzero `n`. -/
@[simps]
def nat.div_mod_equiv (n : ℕ) [ne_zero n] : ℕ ≃ ℕ × fin n :=
{ to_fun := λ a, (a / n, ↑a),
  inv_fun := λ p, p.1 * n + p.2,
  left_inv := λ a, nat.div_add_mod' _ _,
  right_inv := λ p, begin
    refine prod.ext _ (fin.ext $ nat.mul_add_mod_of_lt p.2.is_lt),
    dsimp only,
    rw [add_comm, nat.add_mul_div_right _ _ (ne_zero.pos n), nat.div_eq_zero p.2.is_lt, zero_add],
  end }

(and similarly for int)

[Eric Wieser]

docs#nat.div_mod_unique and docs#int.div_mod_unique are the closest I can find

[Anne Baanen]

Maybe we have the group-theoretical formulation? I can't find anything though...

[Eric Wieser]

The int version can be spelt int.div_mod_equiv (n : ℕ) : ℤ ≃ ℤ × zmod n I think

[Reid Barton]

Wouldn't it be more convenient to just pass (h : n \ne 0)?

[Eric Wieser]

Oh, probably

[Eric Wieser]

Oh, I remember the reason now; ↑a needs ne_zero

[Eric Wieser]

#18359

[Reid Barton]

I think you should not pass the typeclass burden onto the users of nat.div_mod_equiv.

[Eric Wieser]

I would expect that for most cases n is a constant, and so ne_zero is actually more convenient