zmod_congr_of_sub_mem_max_ideal — Mathlib

English

If x - m and x - n lie in the maximal ideal of ℤ_[p], then m ≡ n mod p in ZMod p.

Русский

Если x - m и x - n лежат в максимальном идеале ℤ_[p], то m ≡ n по модулю p в ZMod p.

LaTeX

$$$ (m : ZMod p) = n$ при условиях $x - m \in \\mathfrak{m}$ и $x - n \in \\mathfrak{m}$$$

Lean4

theorem zmod_congr_of_sub_mem_max_ideal (x : ℤ_[p]) (m n : ℕ) (hm : x - m ∈ maximalIdeal ℤ_[p])
    (hn : x - n ∈ maximalIdeal ℤ_[p]) : (m : ZMod p) = n :=
  by
  rw [maximalIdeal_eq_span_p] at hm hn
  have := zmod_congr_of_sub_mem_span_aux 1 x m n
  simp only [pow_one] at this
  specialize this hm hn
  apply_fun ZMod.castHom (show p ∣ p ^ 1 by rw [pow_one]) (ZMod p) at this
  simp only [map_intCast] at this
  simpa only [Int.cast_natCast] using this

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