gammaSet_one_equiv — Mathlib

English

There is a natural equivalence between gammaSet(1,r,a) for any a and the corresponding gammaSet(1,r,a′).

Русский

Существует естественное эквивалентное отображение между gammaSet(1,r,a) и gammaSet(1,r,a′) для любых a, a′.

LaTeX

$$$\gammaSet\_one\_equiv(r,a,a') : \gammaSet(1,r,a) \simeq \gammaSet(1,r,a').$$$

Lean4

/-- For level `N = 1`, the gamma sets are all equivalent; this is the equivalence. -/
def gammaSet_one_equiv (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a ≃ gammaSet 1 r a' :=
  Equiv.setCongr (gammaSet_one_const r a a')

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