inv — Mathlib

English

Integer cast into the p-adics is injective: (z1 : ℤ_p) = z2 iff z1 = z2 (as integers).

Русский

Встраивание целого числа в п-адические числа инъективно: (z1) = z2 эквивалентно z1 = z2 (как целые).

LaTeX

$$$(z_1 : \mathbb{Z}_p) = z_2 \iff z_1 = z_2$$$

Lean4

/-- The inverse of a `p`-adic integer with norm equal to `1` is also a `p`-adic integer.
Otherwise, the inverse is defined to be `0`. -/
def inv : ℤ_[p] → ℤ_[p]
  | ⟨k, _⟩ => if h : ‖k‖ = 1 then ⟨k⁻¹, by simp [h]⟩ else 0

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