English
For any property P on ZMod n, P holds for all residue classes iff P holds for all integers after casting into ZMod n.
Русский
Для любого свойства P на ZMod n справедливо: P выполняется для всех классов по модулю n тогда и только тогда, когда P выполняется для всех целых чисел после приведения к ZMod n.
LaTeX
$$$\\\\forall {n} \\\\forall P : ZMod n \\\\to \\\\mathrm{Prop}, \\\\bigl( \\\\forall x : ZMod n, P x \bigr) \\\\iff \\\\bigl( \\\\forall z : \\\\mathbb{Z}, P z \\\\bmod n \bigr)$$$
Lean4
theorem «forall» {P : ZMod n → Prop} : (∀ x, P x) ↔ ∀ x : ℤ, P x :=
intCast_surjective.forall
