← all areas

Namespace HeckeIntegralSeam 8 theorems

— 6 · IsHeckeCosetSystem 2

directly in HeckeIntegralSeam 6

• Hecke coset sum independent of chosen representatives HeckeIntegralSeam.heckeCosetSum_eq_of_isHeckeCosetSystem 0 below · cited by 33 · depth 11
• Explicit coset system for the Hecke double coset at v HeckeIntegralSeam.exists_isHeckeCosetSystem_localRep_heckeGen 0 below · cited by 40 · depth 16
• Hecke coset system for Uᵥ at a place dividing the level HeckeIntegralSeam.exists_isHeckeCosetSystem_localRepSome_heckeGen_of_dvd 0 below · cited by 1 · depth 19
• Existence of a finite Hecke coset system for diag(varpi,1) HeckeIntegralSeam.exists_isHeckeCosetSystem_integralSubgroup_diagPi 3 below · cited by 3 · depth 24
• Explicit qᵥ+1 Hecke coset representatives at a finite place HeckeIntegralSeam.exists_isHeckeCosetSystem_localRep_heckeGen_principalLevel 0 below · cited by 1 · depth 28
• Common transversal for UgU and its adjoint system HeckeIntegralSeam.exists_isHeckeCosetSystem_and_isHeckeCosetSystem_mul_inv_of_conj_eq 0 below · cited by 2 · depth 30

HeckeIntegralSeam.IsHeckeCosetSystem 2

• Left multiplication by u ∈ U permutes a Hecke coset system HeckeIntegralSeam.IsHeckeCosetSystem.exists_bijective_forall_exists_mul_eq_mul_of_mem 0 below · cited by 1 · depth 20
• Right U-invariance of iterated Hecke words HeckeIntegralSeam.IsHeckeCosetSystem.sum_apply_mul_prod_ofFn_eq_of_mem 0 below · cited by 2 · depth 34