inv_ofNat_num — Mathlib

English

For any a ∈ ℕ with a ≥ 2, the reciprocal of a (embedded in ℚ) has denominator equal to a.

Русский

Пусть a ∈ ℕ, a ≥ 2. Обратное к a в ℚ имеет знаменатель, равный a.

LaTeX

$$$\\forall a \\in \\mathbb{N}, a \\ge 2 \\Rightarrow \\mathrm{den}((\\mathrm{ofNat}(a))^{-1}) = a$$$

Lean4

theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (ofNat(a) : ℚ)⁻¹.num = 1 := by
  -- This proof is quite unpleasant: golf / find better simp lemmas?

  have : 2 ≤ a := Nat.AtLeastTwo.prop
  simp only [num_inv, num_ofNat, den_ofNat, Nat.cast_one, mul_one, Int.sign_eq_one_iff_pos, gt_iff_lt]
  change 0 < (a : ℤ)
  cutsat

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