zmodRepr_unique — Mathlib

English

If y ∈ ℕ satisfies y < p and x − y ∈ maximalIdeal(ℤ_p), then zmodRepr(x) = y; the residue representative is unique among numbers below p.

Русский

Если y ∈ ℕ такe, что y < p и x − y ∈ maximalIdeal(ℤ_p), то zmodRepr(x) = y; остаток по модулю p уникален в диапазоне 0 ≤ y < p.

LaTeX

$$$\forall x \in \mathbb{Z}_{(p)},\; \forall y \in \mathbb{N},\; y < p \Rightarrow (x - y \in \mathfrak{m}_{\mathbb{Z}_{(p)}}) \Rightarrow zmodRepr(x) = y$$$

Lean4

theorem zmodRepr_unique (y : ℕ) (hy₁ : y < p) (hy₂ : x - y ∈ maximalIdeal ℤ_[p]) : zmodRepr x = y :=
  have h := (Classical.choose_spec (existsUnique_mem_range x)).right
  (h (zmodRepr x) (zmodRepr_spec x)).trans (h y ⟨hy₁, hy₂⟩).symm

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