norm_natCast_eq_one_iff — Mathlib

English

For natural n, the norm of its natural embedding in Z_p equals 1 if and only if p is coprime to n.

Русский

Для натурального n норма вложения n в Z_p равна 1 тогда и только тогда, когда p и n взаимно просты.

LaTeX

$$$$\|n\| = 1 \iff p \text{ и } n \text{ взаимно просты}.$$$

Lean4

@[simp]
theorem norm_natCast_eq_one_iff {n : ℕ} : ‖(n : ℤ_[p])‖ = 1 ↔ p.Coprime n := by
  rw [norm_def, coe_natCast, Padic.norm_natCast_eq_one_iff]

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