lean_workbook_plus_29686

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Prove that $a_i$ =i for all i given $a_0,a_1,\dots,a_n$ is a sequence of positive integers such that: ( $a_i,a_j$ )=( $i,j$ ) for all i $\neq$ j.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29686 {n : ℕ} (a : ℕ → ℕ) (h₀ : ∀ i, 0 < a i) (h₁ : ∀ i j, i ≠ j → (a i, a j) = (i, j)) : ∀ i, a i = i   :=  by sorry

Source