den_div_intCast_eq_one_iff — Mathlib

English

For m,n ∈ ℤ with n ≠ 0, the statement ((m : ℚ) / n).den = 1 holds if and only if n ∣ m.

Русский

Для m, n ∈ ℤ, n ≠ 0, верно: знаменатель дроби (m/n) равен 1 тогда и только тогда, когда n делит m.

LaTeX

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

Lean4

theorem den_div_intCast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m :=
  by
  replace hn : (n : ℚ) ≠ 0 := num_ne_zero.mp hn
  constructor
  · rw [Rat.den_eq_one_iff, eq_div_iff hn]
    exact mod_cast (Dvd.intro_left _)
  · exact (intCast_div _ _ · ▸ rfl)

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