natCast_dvd — Mathlib

English

For any m ∈ ℕ and n ∈ ℤ, m divides n in ℤ if and only if m divides |n| in ℕ.

Русский

Для любых m ∈ ℕ и n ∈ ℤ верна эквивалентность: m делится на n в ℤ тогда и только тогда, когда m делится на |n| в ℕ.

LaTeX

$$$\\\\forall m \\in \\mathbb{N},\\\\forall n \\in \\mathbb{Z},\\\\quad m \\mid n \\iff m \\mid |n|$$

Lean4

theorem natCast_dvd {m : ℕ} : (m : ℤ) ∣ n ↔ m ∣ n.natAbs := by
  obtain hn | hn := natAbs_eq n <;> rw [hn] <;> simp [← natCast_dvd_natCast, Int.dvd_neg]

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