About the type of the arguments for Int.mod_coprime

Stream: mathlib4

[Kevin Cheung]

I saw that Int.mod_coprime has type Nat for the arguments a and b:

theorem Int.mod_coprime{a b : ℕ} (hab : a.Coprime b) :
∃ (y : ℤ), ↑a * y ≡ 1 [ZMOD ↑b]

Since this theorem is under Mathlib.Data.Int.ModEq, I was expecting that a and b would be Int. Is such an expectation reasonable?

Also, would a Nat version look like the following?

theorem Nat.mod_coprime{a b : ℕ} (hab : a.Coprime b) :
∃ y , a * y ≡ 1 [MOD b]

[Aaron Liu]

docs#Int.mod_coprime

[Aaron Liu]

I don't like this because it doesn't follow the naming convention

[Kevin Cheung]

How should this be fixed?

[Ruben Van de Velde]

Fwiw, this works:

import Mathlib

open Int

theorem mod_coprime {a b : ℤ} (hab : IsCoprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
  ⟨Int.gcdA a b,
    have hgcd : Int.gcd a b = 1 := Int.isCoprime_iff_gcd_eq_one.mp hab
    calc
      a * Int.gcdA a b ≡ a * Int.gcdA a b + b * Int.gcdB a b [ZMOD b] :=
        ModEq.symm <| modEq_add_fac _ <| ModEq.refl _
      _ ≡ 1 [ZMOD b] := by rw [← Int.gcd_eq_gcd_ab, hgcd, Nat.cast_one]
      ⟩

[Kevin Cheung]

Thanks @Ruben Van de Velde . Will you make this change for a future release of Mathlib?

[Ruben Van de Velde]

I wasn't planning to, but anyone should feel free :)