zmod_congr_of_sub_mem_span_aux — Mathlib

English

If x ≡ a (mod p^n) and x ≡ b (mod p^n) in the p-adic integers, then a ≡ b in ZMod(p^n).

Русский

Если x ≡ a (mod p^n) и x ≡ b (mod p^n) в p-адических целых, то a ≡ b в ZMod(p^n).

LaTeX

$$$(a : \\mathbb{Z}/p^n\\mathbb{Z}) = b$ при условиях x-a ∈ (p^n) и x-b ∈ (p^n)$$

Lean4

theorem zmod_congr_of_sub_mem_span_aux (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
  rw [Ideal.mem_span_singleton] at ha hb
  rw [← sub_eq_zero, ← Int.cast_sub, ZMod.intCast_zmod_eq_zero_iff_dvd, Int.natCast_pow]
  rw [← dvd_neg, neg_sub] at ha
  have := dvd_add ha hb
  rwa [sub_eq_add_neg, sub_eq_add_neg, add_assoc, neg_add_cancel_left, ← sub_eq_add_neg, ← Int.cast_sub,
    pow_p_dvd_int_iff] at this

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