English
Let p be a prime. For every nonzero element x in the p-adic integers Z_p, x can be written as a unit times p raised to the p-adic valuation of x; i.e., there exists a unit u in Z_p with x = u · p^{v_p(x)} (where v_p is the p-adic valuation).
Русский
Пусть p — простое число. Для любого ненулевого элемента x в p-адических целых числах Z_p существует единица u в Z_p такая, что x = u · p^{v_p(x)} (где v_p — p-адическая характеристика).
LaTeX
$$$\forall x \in \mathbb{Z}_p,\ x \neq 0 \Rightarrow \exists u \in (\mathbb{Z}_p)^{\times},\ x = u\, p^{\nu_p(x)}.$$$
Lean4
theorem unitCoeff_spec {x : ℤ_[p]} (hx : x ≠ 0) : x = (unitCoeff hx : ℤ_[p]) * (p : ℤ_[p]) ^ x.valuation :=
by
apply Subtype.coe_injective
push_cast
rw [unitCoeff_coe, mul_assoc, ← zpow_natCast, ← zpow_add₀]
· simp
· exact NeZero.ne _
