English
Let p be a prime. The p-adic integers ℤ_p can be realized as the subring of ℚ_p consisting of all elements with p-adic norm at most 1.
Русский
Пусть p является перовым. p-адические целые ℤ_p можно рассматривать как подкольцо ℚ_p, состоящее из элементов с p-адической нормой не более 1.
LaTeX
$$$\mathbb{Z}_p = \{ x \in \mathbb{Q}_p \mid \|x\|_p \le 1 \}$$$
Lean4
/-- The `p`-adic integers as a subring of `ℚ_[p]`. -/
def subring : Subring ℚ_[p] where
carrier := {x : ℚ_[p] | ‖x‖ ≤ 1}
zero_mem' := by simp
one_mem' := by simp
add_mem' hx hy := (Padic.nonarchimedean _ _).trans <| max_le_iff.2 ⟨hx, hy⟩
mul_mem' hx hy := (padicNormE.mul _ _).trans_le <| mul_le_one₀ hx (norm_nonneg _) hy
neg_mem' hx := (norm_neg _).trans_le hx
