dvd_natCast — Mathlib

English

For all m,n ∈ ℕ, m divides n in ℕ if and only if m divides n when viewed in ℤ after casting.

Русский

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

LaTeX

$$$\\\\forall m,n \\in \\mathbb{N},\\\\quad m \\mid n \\text{ (in } \\mathbb{N}) \iff m \\mid n \\text{ (in } \\mathbb{Z} \\text{ after casting)}$$$

Lean4

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

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