English
For any a,b, (a : R) = (b : R) iff a ≡ b (mod p).
Русский
Для любых a,b: (a:R) = (b:R) тогда и только тогда, когда a ≡ b (mod p).
LaTeX
$$$(a : R) = (b : R) \iff a \equiv b \pmod p$$$
Lean4
theorem cast_eq_iff_mod_eq [IsLeftCancelAdd R] : (a : R) = (b : R) ↔ a % p = b % p :=
by
wlog hle : a ≤ b
· simpa only [eq_comm] using (this _ _ (lt_of_not_ge hle).le)
obtain ⟨c, rfl⟩ := Nat.exists_eq_add_of_le hle
rw [Nat.cast_add, left_eq_add, CharP.cast_eq_zero_iff R p]
constructor
· simp +contextual [Nat.add_mod, Nat.dvd_iff_mod_eq_zero]
intro h
have := Nat.sub_mod_eq_zero_of_mod_eq h.symm
simpa [Nat.dvd_iff_mod_eq_zero] using this