gammaSetDivGcdEquiv_eq — Mathlib

English

There is an equivalence between the space of functions Fin 2 → ℤ and the sigma-type of natural numbers paired with a gammaSet: Fin 2 → ℤ ≃ Σ r γSet 1 r 0.

Русский

Существует эквивалентность между пространством отображений Fin 2 → ℤ и сигма-типом натуральных чисел в паре с гамма-набором: Fin 2 → ℤ ≃ Σ r γSet 1 r 0.

LaTeX

$$$\gammaSetDivGcdSigmaEquiv : (\mathbb{F}\!in\ 2 \to \mathbb{Z}) \simeq \sum_{r \in \mathbb{N}} \gammaSet(1,r,0).$$$

Lean4

@[simp]
theorem gammaSetDivGcdEquiv_eq (r : ℕ) [NeZero r] (v : gammaSet 1 r 0) : (gammaSetDivGcdEquiv r) v = divIntMap r v.1 :=
  rfl

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