gammaSet_one_const — Mathlib

English

For level N = 1, all gammaSet(1,r,a) are the same for all a; the level 1 gamma-sets do not depend on a.

Русский

Для уровня N = 1 гамма-множества gammaSet(1,r,a) не зависят от a; все они равны.

LaTeX

$$$\gammaSet(1,r,a)=\gammaSet(1,r,a') \quad \text{for all } a,a'.$$$

Lean4

/-- For level `N = 1`, the gamma sets are all equal. -/
theorem gammaSet_one_const (a a' : Fin 2 → ZMod 1) : gammaSet 1 r a = gammaSet 1 r a' :=
  congr_arg _ (Subsingleton.elim _ _)

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