natCast_eq_iff — Mathlib

English

For p, n, z ∈ ZMod p with p ≠ 0, equality n = z.cast modulo p holds iff there exists k with n = z.val + p k.

Русский

Для p>0 и z ∈ ZMod p равенство n = z.cast по модулю p эквивалентно существованию k: n = z.val + p k.

LaTeX

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

Lean4

theorem natCast_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_natCast, Nat.mod_add_div]
  · rintro ⟨k, rfl⟩
    rw [Nat.cast_add, natCast_zmod_val, Nat.cast_mul, natCast_self, zero_mul, add_zero]

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