X mod N mod D v X mod D

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this?

import Mathlib.Data.Nat.ModEq
import Mathlib.Data.ZMod.Algebra

example (D N : ℕ) (h : D ∣ N) (e : ZMod N) : e.val ≡ (ZMod.castHom h _ e : ZMod D).val [MOD D] := sorry

I need it for Fermat's Last Theorem :-)

[Ruben Van de Velde]

import Mathlib.Data.Nat.ModEq
import Mathlib.Data.ZMod.Algebra

example (D N : ℕ) (h : D ∣ N) (e : ZMod N) : e.val ≡ (ZMod.castHom h _ e : ZMod D).val [MOD D] := by
  simp
  have : NeZero N := sorry
  rw [ZMod.cast_eq_val]
  rw [@ZMod.val_natCast]
  rw [@Nat.ModEq.comm]
  exact Nat.mod_modEq e.val D

[Kevin Buzzard]

Oh thanks! In the application N is indeed positive (unsurprisingly this is a ZHat thing).

[Ruben Van de Velde]

(I guessed as much, and have no idea if it's true for 0 anyway)