beta_unbeta_coe — Mathlib

English

For any list l and i ∈ Fin(length l), beta(unbeta(l), i) equals the i-th element of l.

Русский

Для любого списка l и i ∈ Fin(|l|) β(unbeta(l), i) равно i-му элементу l.

LaTeX

$$$\\beta(\\mathrm{unbeta}(l), i) = l[i]$ for $i : \\mathrm{Fin}(l.length)$$$

Lean4

/-- **Gödel's Beta Function Lemma** -/
theorem beta_unbeta_coe (l : List ℕ) (i : Fin l.length) : beta (unbeta l) i = l[i] := by
  simpa [beta, unbeta, coprimes] using
    mod_eq_of_modEq
      ((chineseRemainderOfFinset (l[·]) (coprimes (l[·])) Finset.univ (by simp [coprimes])
            (by simpa using Set.pairwise_univ.mpr (pairwise_coprime_coprimes _))).prop
        i (by simp))
      (coprimes_lt _ _)

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