ofNat_dvd_natCast — Mathlib

English

Let x,y be natural numbers. The divisibility of their natural embedding into integers coincides with their natural divisibility: the integer ι(x) divides ι(y) if and only if x divides y in N.

Русский

Пусть x,y ∈ ℕ. Делимость их образов в ℤ совпадает с делимостью в ℕ: ι(x) делится на ι(y) в ℤ тогда и только тогда, когда x делится на y в ℕ.

LaTeX

$$$\\\\forall x,y \in \mathbb{N},\\\\quad \iota(x) \mid \ iota(y) \iff x \mid y$$$

Lean4

@[norm_cast]
theorem ofNat_dvd_natCast {x y : ℕ} : (ofNat(x) : ℤ) ∣ (y : ℤ) ↔ OfNat.ofNat x ∣ y :=
  natCast_dvd_natCast

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