natCast_dvd_ofNat — Mathlib

English

Let x,y ∈ ℕ. The divisibility of the integer x by the integer representation of y matches the natural divisibility: (x : ℤ) | (ofNat y : ℤ) iff x | y.

Русский

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

LaTeX

$$$\\\\forall x,y \in \mathbb{N},\\\\quad (x : \\mathbb{Z}) \\mid (\\operatorname{ofNat}(y) : \\mathbb{Z}) \iff x \\mid y$$$

Lean4

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

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