norm_intCast_eq_one_iff — Mathlib

English

For z ∈ Z, the p-adic norm of its embedding into Z_p equals 1 iff z is coprime to p (IsCoprime).

Русский

Для z ∈ Z нормa p-адических вложений в Z_p равна 1 тогда и только тогда, когда z и p взаимно просты (IsCoprime).

LaTeX

$$$$\|z\| = 1 \iff \text{IsCoprime}(z, p).$$$$

Lean4

@[simp]
theorem norm_intCast_eq_one_iff {z : ℤ} : ‖(z : ℤ_[p])‖ = 1 ↔ IsCoprime z p := by
  rw [norm_def, coe_intCast, Padic.norm_intCast_eq_one_iff]

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