den_div_natCast_eq_one_iff — Mathlib

English

For m,n ∈ ℕ with n ≠ 0, the equation ((m : ℚ) / n).den = 1 is equivalent to n ∣ m, via the natCast embedding.

Русский

Для m,n ∈ ℕ, n ≠ 0, равносильно: деноминированный м/н равен 1 тогда и только тогда, когда n делит m.

LaTeX

$$$( (m : \\mathbb{Q}) / n ).den = 1 \\iff n \\mid m$$$

Lean4

theorem den_div_natCast_eq_one_iff (m n : ℕ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m :=
  (den_div_intCast_eq_one_iff m n (Int.ofNat_ne_zero.mpr hn)).trans Int.ofNat_dvd

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