zmod.nat_cast_eq_iff

Stream: Is there code for X?

[Eric Wieser]

Do we have anything like this?

import data.zmod.basic

namespace zmod

lemma nat_cast_eq_iff (p : ℕ) (n : ℕ) (z : zmod p) [fact (0 < p)] :
  ↑n = z ↔ ∃ k, n = z.val + p * k :=
begin
  split,
  { rintro rfl,
    refine ⟨n / p, _⟩,
    rw [val_nat_cast, nat.mod_add_div] },
  { rintro ⟨k, rfl⟩,
    rw [nat.cast_add, nat_cast_zmod_val, nat.cast_mul, nat_cast_self, zero_mul, add_zero] }
end

end zmod

We have docs#zmod.nat_coe_eq_nat_coe_iff and zmod.nat_coe_eq_nat_coe_iff', but I can't see an obvious way to use those in this proof

[Reid Barton]

Don't know, but I'm pretty sure you don't need [fact (0 < p)]

[Eric Wieser]

The reverse direction is not true for p = 0, since z.val = int.nat_abs z in that case

[Reid Barton]

oh the reverse. Yeah that function is dumb

[Eric Wieser]

Relatedly, is this lemma true?

lemma val_int_cast {n : ℕ} (a : ℤ) [fact (0 < n)] : ↑(a : zmod n).val = a % n :=

I'm struggling to juggle all the casts going on here

[Eric Rodriguez]

does docs#zmod.int_cast_mod help?

[Eric Rodriguez]

I was going to say that I used similar lemmas when working on the galois group of cyclotomic extensions, but I ended up just using modeq as zmod was too much of a pain

[Kevin Buzzard]

Is there missing API for zmod?

[Eric Wieser]

Eric Rodriguez said:

does docs#zmod.int_cast_mod help?

I can't work out how to use it here

[Kevin Buzzard]

import data.zmod.algebra

theorem zmod.mod_eq_of_modeq (a b : ℤ) (n : ℕ)
  (h1 : a ≡ b [ZMOD n]) (h2 : 0 ≤ a) (h3 : a < n) : b % n = a :=
begin
  -- I'm sure this can be golfed
  rw ← int.mod_eq_of_lt h2 h3,
  exact eq.symm h1,
end

lemma val_int_cast {n : ℕ} (a : ℤ) [fact (0 < n)] : ↑(a : zmod n).val = a % n :=
begin
  rw zmod.mod_eq_of_modeq,
  { exact ((zmod.int_coe_eq_int_coe_iff' a _ n).mp (by simp)).symm },
  { exact int.coe_nat_nonneg _ },
  { exact_mod_cast zmod.val_lt _, apply_instance, }
end

[Eric Wieser]

#12571