inv_intCast_den_of_pos — Mathlib

English

For any a ∈ ℤ with a > 0, the denominator of (a : ℚ)⁻¹ equals a.

Русский

Для любого a ∈ ℤ, a > 0, знаменатель (a : ℚ)⁻¹ равен a.

LaTeX

$$$((a : \\mathbb{Q})^{-1}.den : \\mathbb{Z}) = a$$$

Lean4

theorem inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a :=
  by
  rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_divInt, divInt_eq_div, Nat.cast_one]
  apply den_div_eq_of_coprime ha0
  rw [Int.natAbs_one]
  exact Nat.coprime_one_left _

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