inv_ofNat_den — Mathlib

English

For any q ≠ 0 in ℚ, the denominator of q⁻¹ equals the absolute value of the numerator of q.

Русский

Для любого q ≠ 0 в ℚ знаменатель q⁻¹ равен абсолютному значению числителя q.

LaTeX

$$$\\forall q \\in \\mathbb{Q}, q \\neq 0 \\Rightarrow (q^{-1}).den = |q_{num}|$$$

Lean4

theorem inv_ofNat_den (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.den = OfNat.ofNat a := by
  simp [den_inv, Int.natAbs_eq_iff]

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