About the naming of `Int.existsUnique_equiv`

Stream: mathlib4

[Kevin Cheung]

I wonder if something is missing in

theorem Int.existsUnique_equiv(a : ℤ) {b : ℤ} (hb : 0 < b) :
∃ (z : ℤ), 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]

Since the word "Unique" is in the name, should the theorem have ∃! (z : ℤ)?

[Ruben Van de Velde]

I think it should be renamed to exists_unique_equiv like it was in mathlib3, and it's called existsUnique only due to some overzealous translating in the port

[Aaron Liu]

I don't see what the unique part is referring to, this only seems to be proving existence within certain bounds.

[Violeta Hernández]

Aaron Liu ha dicho:

I don't see what the unique part is referring to, this only seems to be proving existence within certain bounds.

I get your point, but I'm not sure if exists_nonneg_lt_equiv or whatnot would be a better name.

[Weiyi Wang]

Why don't we upgrade this to a existsUnique lemma, though? It is true, right?

[Violeta Hernández]

I think the idea is we don't like writing existsUnique lemmas because most of them hint at a missing function (in this case, that function is just a % b)

[Yury G. Kudryashov]

Also, it should be modEq, not equiv.

[Kevin Cheung]

I think it is useful to have a result that asserts such a unique integer modulo b exists.

[Kevin Buzzard]

I think it would be more useful to have two results, one saying existence and another one saying uniqueness. We typically don't have theorems in the library of the form "X and Y".

[Kevin Cheung]

Something like this?

theorem foo {b r s : ℤ} (hr : 0 ≤ r ∧ r < b) (hs : 0 ≤ s ∧ s < b)
  (h : r ≡ s [ZMOD b]) : r = s := sorry

[Robin Arnez]

I think that is a consequence of docs#Int.ext_ediv_modEq and docs#Int.ediv_eq_zero_of_lt:

import Mathlib

theorem foo {b r s : ℤ} (hr : 0 ≤ r ∧ r < b) (hs : 0 ≤ s ∧ s < b)
    (h : r ≡ s [ZMOD b]) : r = s :=
  Int.ext_ediv_modEq (by simp [Int.ediv_eq_zero_of_lt, *]) h

[Kevin Buzzard]

Kevin Cheung said:

Something like this?

Yes except that we don't usually have hypotheses of the form A and B either :-) (we just have more hypotheses)