Z/nZ = zmod?

Stream: Is there code for X?

[Scott Morrison]

Is this hiding somewhere in mathlib that I'm not finding?

def quotient_gsmul (k : ℕ) :
  quotient_add_group.quotient (set.range (gsmul k : ℤ → ℤ)) ≃+ zmod k :=
sorry