cast_eq_iff_mod_eq — Mathlib

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

Похожие утверждения