dvd_natAbs_of_coe_dvd_sq — Mathlib

English

Let p be prime, k ∈ ℤ, and p divides k^2 in ℤ. Then p divides |k|, i.e., p ∣ k.natAbs.

Русский

Пусть p — простое число, k ∈ ℤ, и p делит k^2 в ℤ. Тогда p делит |k|, то есть p делит natAbs(k).

LaTeX

$$$\forall p \in \mathbb{N}, \mathrm{Prime}(p) \to \forall k \in \mathbb{Z}, (p \mid k^2) \to p \mid k.\mathrm{natAbs}.$$$

Lean4

theorem dvd_natAbs_of_coe_dvd_sq {p : ℕ} (hp : p.Prime) (k : ℤ) (h : (p : ℤ) ∣ k ^ 2) : p ∣ k.natAbs :=
  by
  apply @Nat.Prime.dvd_of_dvd_pow _ _ 2 hp
  rwa [sq, ← natAbs_mul, ← natCast_dvd, ← sq]

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