den_div_eq_of_coprime — Mathlib

English

Let a,b ∈ ℤ with 0 < b and Nat.Coprime a.natAbs b.natAbs. Then the denominator of (a / b) in ℚ equals b.

Русский

Пусть a,b ∈ ℤ, 0 < b и Nat.Coprime(a.natAbs, b.natAbs). Тогда знаменатель дроби a/b в ℚ равен b.

LaTeX

$$$0 < b \\land Nat.Coprime(a.natAbs, b.natAbs) \\Rightarrow ((a / b : \\mathbb{Q}).den) = b$$$

Lean4

theorem den_div_eq_of_coprime {a b : ℤ} (hb0 : 0 < b) (h : Nat.Coprime a.natAbs b.natAbs) : ((a / b : ℚ).den : ℤ) = b :=
  by
  lift b to ℕ using hb0.le
  simp only [Int.natAbs_natCast, Int.natCast_pos] at h hb0
  rw [← Rat.divInt_eq_div, ← mk_eq_divInt _ _ hb0.ne' h]

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