pow_p_dvd_int_iff — Mathlib

English

For n ∈ ℕ and a ∈ ℤ, (p^n) divides a in the p-adic integers Z_p if and only if p^n divides a in ℤ.

Русский

Для n ∈ ℕ и a ∈ ℤ: p^n делит a в Z_p тогда и только тогда, когда p^n делит a в ℤ.

LaTeX

$$$\forall n\in\mathbb{N},\forall a\in\mathbb{Z},\ (p^n:\mathbb{Z}_p)\mid a \iff (p^n:\mathbb{Z})\mid a.$$

Lean4

@[simp]
theorem pow_p_dvd_int_iff (n : ℕ) (a : ℤ) : (p : ℤ_[p]) ^ n ∣ a ↔ (p ^ n : ℤ) ∣ a := by
  rw [← Nat.cast_pow, ← norm_int_le_pow_iff_dvd, norm_le_pow_iff_mem_span_pow, Ideal.mem_span_singleton, Nat.cast_pow]

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