intCast_eq_iff — Mathlib

English

For any p, n, z ∈ ZMod p with p ≠ 0, ↑n = z iff there exists k with n = z.val + p k.

Русский

Для любых p>0, n ∈ ℤ и z ∈ ZMod p, ↑n = z тогда существует k: n = z.val + p k.

LaTeX

$$$\forall p\ n\ z\ [NeZero p],\ ↑n = z \iff \exists k, n = z.{\tt val} + p k$$$

Lean4

theorem intCast_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] : ↑n = z ↔ ∃ k, n = z.val + p * k :=
  by
  constructor
  · rintro rfl
    refine ⟨n / p, ?_⟩
    rw [val_intCast, Int.emod_add_mul_ediv]
  · rintro ⟨k, rfl⟩
    rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val, ZMod.natCast_self, zero_mul,
      add_zero, cast_id]

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