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