how to use absolute value in a place

Stream: new members

[Chengyan Hu]

Hi! Lean believe the absolute value here is an integer, but I need my input to be a natural number to make it work. I stuck on how to change it to an natural number.

import Mathlib
open Ideal Padic Nat ZMod
open scoped algebraMap

variable
    {K:Type*}[Field K]
    (ζ:K)(n:ℕ)(a b: ZMod (n))(hζ:IsPrimitiveRoot ζ n)

include hζ in
theorem pow_eq_ex_eq: ζ^(a.val)=ζ^(b.val) ↔ a=b := by
  constructor
  rintro h
  have h1:ζ^(abs ((b.val:ℤ)-(a.val:ℤ)))=1 := by
    sorry
  have h2:=hζ.dvd_of_pow_eq_one
  specialize h2 (abs ((b.val:ℤ)-(a.val:ℤ))) h1
  have: a.val ≡ b.val [MOD n]:= by
    rw[modEq_iff_dvd]
    exact h2

[Weiyi Wang]

To solve the immediate problem, because h2 expect a Nat, while abs always expect the input and the output to be the same type, it deduces that b.val should be Nat as well. To convert Int to Nat while doing abs, you can use Int.natAbs instead.
Though, this now generates other errors which I haven't looked into yet

[Weiyi Wang]

You can then use Nat.cast_natAbs to convert between the two versions of abs