existsUnique_mem_range — Mathlib

English

For PadicInt x, there exists a unique n with n < p and x − n in the maximal ideal.

Русский

Для PadicInt x существует единственное n, с n < p и x − n ∈ максимальный идеал.

LaTeX

$$$\\\\exists! n \\\\in \\\\mathbb{N}, n < p \\\\land x - n \\\\in maximalIdeal(\\\\mathbb{Z}_{p})$$$

Lean4

theorem existsUnique_mem_range : ∃! n : ℕ, n < p ∧ x - n ∈ maximalIdeal ℤ_[p] :=
  by
  obtain ⟨n, hn₁, hn₂⟩ := exists_mem_range x
  use n, ⟨hn₁, hn₂⟩, fun m ⟨hm₁, hm₂⟩ ↦ ?_
  have := (zmod_congr_of_sub_mem_max_ideal x n m hn₂ hm₂).symm
  rwa [ZMod.natCast_eq_natCast_iff, ModEq, mod_eq_of_lt hn₁, mod_eq_of_lt hm₁] at this

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