zmod_congr_of_sub_mem_span — Mathlib

English

If x - a and x - b lie in the span of p^n, then a and b are congruent mod p^n in ZMod.

Русский

Если x - a и x - b принадлежат порождающему множеству p^n, то a ≡ b (mod p^n) в ZMod.

LaTeX

$$$ (a : ZMod(p^n)) = b$ при условии $x - a \in \\langle p^n \\rangle$ и $x - b \in \\langle p^n \\rangle$$$

Lean4

theorem zmod_congr_of_sub_mem_span (n : ℕ) (x : ℤ_[p]) (a b : ℕ) (ha : x - a ∈ (Ideal.span {(p : ℤ_[p]) ^ n}))
    (hb : x - b ∈ (Ideal.span {(p : ℤ_[p]) ^ n})) : (a : ZMod (p ^ n)) = b := by
  simpa using zmod_congr_of_sub_mem_span_aux n x a b ha hb

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