intCast_modEq_intCast — Mathlib

English

Let α be a type with AddCommGroupWithOne structure and CharZero. For all integers a, b and z, a is congruent to b modulo z after casting z into α if and only if a is congruent to b modulo z in the integers.

Русский

Пусть α — множество с добавочно-коммутативной группой и единицей, характеристика ноль, и целые a, b, z. Тогда a ≡ b (mod z), когда z приводится к α, тогда и только тогда a ≡ b (mod z) в ℤ.

LaTeX

$$$ a \equiv b \ [PMOD (z : \alpha)] \iff a \equiv b \ [PMOD z] $$$

Lean4

@[simp, norm_cast]
theorem intCast_modEq_intCast {a b z : ℤ} : a ≡ b [PMOD (z : α)] ↔ a ≡ b [PMOD z] :=
  by
  simp_rw [ModEq, ← Int.cast_mul_eq_zsmul_cast]
  norm_cast

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