← all areas

Namespace HeckeCharacter 28 theorems

— 25 · IsFiniteOrderHeckeChar 3

directly in HeckeCharacter 25

• Idelic Hecke character attached to a Dirichlet character mod qᵇ HeckeCharacter.exists_isFiniteOrderHeckeChar_rat_apply_uniformizerIdele_eq_apply_localUnit_eq_inv 2 below · cited by 6 · depth 13
• Finite-order Hecke character with prescribed values and signs HeckeCharacter.exists_isFiniteOrderHeckeChar_apply_uniformizerIdele_eq_archLocalChar_neg_one_eq_of_raySymbol_eq_prod 9 below · cited by 2 · depth 15
• Idelic first-inequality data for cyclic extensions of degree dividing 24 HeckeCharacter.ideleFirstIneqDataAt_of_isCyclic 64 below · cited by 6 · depth 15
• Finite-order idèle characters kill totally positive infinite idèles HeckeCharacter.apply_eq_one_of_isOfFinOrder_of_archSign 0 below · cited by 4 · depth 16
• Real component of a principal idèle equals τ(α) HeckeCharacter.archRealProjTau_unitsMap_algebraMap 0 below · cited by 3 · depth 16
• Content of a principal idèle is the principal fractional ideal HeckeCharacter.coe_fadContentHom_projFin_unitsMap_algebraMap 2 below · cited by 4 · depth 16
• Integers ≡ 1 mod f with prescribed real signs HeckeCharacter.exists_ne_zero_sub_one_mem_forall_pos_iff 0 below · cited by 2 · depth 16
• Content of an idelic norm is the relative norm of the content HeckeCharacter.fadContentHom_projFin_idelicNorm_eq_fracRelNormUnit 3 below · cited by 7 · depth 16
• Adjusters descend along the idelic norm HeckeCharacter.isAdjuster_idelicNorm_of_isAdjuster 3 below · cited by 7 · depth 16
• Ideal membership as a local condition at the primes dividing f HeckeCharacter.mem_iff_forall_valued_algebraMap_finiteAdeleRing_le 0 below · cited by 6 · depth 16
• Ray symbol of the content of a finite idèle HeckeCharacter.raySymbolUnitsHom_fadContentHom 2 below · cited by 3 · depth 16
• Sign at a real place of a principal translate of an idèle HeckeCharacter.archSign_unitsMap_algebraMap_mul_iff 1 below · cited by 3 · depth 17
• Multiplicity at w of the content of a finite idèle HeckeCharacter.count_coe_fadContentHom 1 below · cited by 6 · depth 17
• Idele class characters determined by almost all uniformizer values HeckeCharacter.eq_of_forall_apply_localUnit_uniformizerUnit_eq 2 below · cited by 6 · depth 17
• A finite-order continuous Hecke character admits a modulus HeckeCharacter.exists_admitsModulus_of_continuous_of_isOfFinOrder 0 below · cited by 1 · depth 17
• Content of a 1-adjusted idèle is coprime to f HeckeCharacter.fadContentHom_projFin_mem_coprimeToModulus_of_isAdjuster_one 3 below · cited by 4 · depth 17
• Signed ray law for a finite-order Hecke character on principal ideals HeckeCharacter.raySymbol_apply_uniformizerIdele_eq_prod_archLocalChar_neg_one_of_admitsModulus 7 below · cited by 2 · depth 17
• Existence of adjusters for idèles at level f HeckeCharacter.exists_isAdjuster 5 below · cited by 5 · depth 18
• Fractional ideals coprime to f as contents of 1-adjusted idèles HeckeCharacter.exists_isAdjuster_one_and_fadContentHom_projFin_eq 2 below · cited by 2 · depth 18
• Content of a finite idèle is coprime to f iff locally unit HeckeCharacter.fadContentHom_mem_coprimeToModulus_iff 2 below · cited by 2 · depth 18
• Relative norm of the content of a principal idèle HeckeCharacter.fracRelNormUnit_fadContentHom_projFin_unitsMap_algebraMap 3 below · cited by 1 · depth 18
• Finite weak approximation at a modulus for idèles HeckeCharacter.exists_forall_dvd_valued_mul_inv_eq_one_and_le 0 below · cited by 1 · depth 19
• Admissible Hecke character of ℚ with prescribed local components HeckeCharacter.exists_isAdmissibleTwist_localChar_eq_of_hasConductorExponentAt 6 below · cited by 7 · depth 21
• Base change preserves 1-adjusted idèles at the extended modulus HeckeCharacter.isAdjuster_unitsMap_genuineBaseChange_one_of_isAdjuster_one 0 below · cited by 1 · depth 24
• Uniform modulus for idele characters with prescribed ramification HeckeCharacter.exists_ne_bot_forall_admitsModulus_of_isUnramifiedCharAt_of_localChar_eq 0 below · cited by 1 · depth 29

HeckeCharacter.IsFiniteOrderHeckeChar 3

• Finite-order Hecke characters of ℚ of modulus (N) are Dirichlet HeckeCharacter.IsFiniteOrderHeckeChar.exists_dirichletIdeleChar_eq_of_admitsModulus 0 below · cited by 3 · depth 14
• Finite-order Hecke characters of ℚ come from Dirichlet characters HeckeCharacter.IsFiniteOrderHeckeChar.exists_dirichletIdeleChar_eq 2 below · cited by 2 · depth 17
• Finite-order Hecke characters of ℚ admit a modulus (N) HeckeCharacter.IsFiniteOrderHeckeChar.exists_admitsModulus 0 below · cited by 1 · depth 18