← all areas

Namespace ArtinL 36 theorems

— 12 · Abelian 24

directly in ArtinL 12

• Tame case: Artin conductor exponent plus inertia invariants equal n ArtinL.conductorExponent_add_finrank_inertiaInvariants_eq 3 below · cited by 1 · depth 11
• Independence of the Artin Euler factor at p from place and Frobenius ArtinL.eulerFactorAt_eq_eulerFactor 2 below · cited by 2 · depth 11
• Functional equation for odd two-dimensional Artin L-functions ArtinL.exists_completedLSeries_functionalEquation_of_odd 377 below · cited by 1 · depth 11
• Absolute convergence of Artin L-series for Re(s)>1 ArtinL.LSeriesSummable_coeff_of_one_lt_re 0 below · cited by 2 · depth 12
• Conductor–discriminant relation for virtual sums of induced characters ArtinL.conductor_mul_prod_pow_eq_prod_pow_of_trace_eq_sum 55 below · cited by 1 · depth 12
• Artin L-series and induced characters on Re s>1 ArtinL.lSeries_mul_prod_pow_eq_prod_pow_of_trace_eq_sum 19 below · cited by 1 · depth 12
• Rational Artin conductor exponent as a character sum ArtinL.codimInvariants_add_swanConductor_eq_finsum_card_mul_sub_sum_trace_of_comp_restrictNormalHom 34 below · cited by 1 · depth 13
• Artin's Euler factor at p from induced characters ArtinL.eulerFactor_mul_prod_pow_eq_prod_pow_of_trace_eq_sum 14 below · cited by 1 · depth 13
• Local conductor–discriminant formula for an induced character ArtinL.finsum_card_mul_sub_sum_induced_eq_factorization_discr_mul_absNorm_conductor 34 below · cited by 1 · depth 13
• Euler product for an Artin L-series at a point of summability ArtinL.hasProd_inv_eval_eulerFactor_of_lSeriesSummable 0 below · cited by 1 · depth 13
• Artin Euler factor computed at a finite Galois level ArtinL.eulerFactor_eq_charpolyRev_restrict_arithFrobAt 8 below · cited by 1 · depth 14
• Trace on invariants as average of traces over a finite subgroup ArtinL.trace_restrict_invariants_eq_inv_card_mul_sum_trace 0 below · cited by 2 · depth 14

ArtinL.Abelian 24

• Functional equation for abelian Artin L-series ArtinL.Abelian.exists_completedLSeries_functionalEquation_u0 335 below · cited by 1 · depth 12
• Induced character at complex conjugation equals n₊-n₋ ArtinL.Abelian.induced_apply_isConj_eq_nPlus_sub_nMinus 0 below · cited by 1 · depth 12
• Euler product and non-vanishing of abelian Artin L-series ArtinL.Abelian.lSeriesSummable_and_lSeries_ne_zero_and_hasProd 0 below · cited by 3 · depth 12
• Primitive narrow ray class character attached to a Galois character ArtinL.Abelian.exists_narrowRayClassChar_conductor_eq_localValue_u0 328 below · cited by 1 · depth 13
• Abelian Artin L-series as Euler product over rational primes ArtinL.Abelian.hasProd_primes_inv_eval_prod_placesOver 1 below · cited by 1 · depth 13
• Abelian Artin L-series equals a narrow ray class L-series ArtinL.Abelian.lSeries_eq_rayClassLSeries_of_eq_localValue 0 below · cited by 1 · depth 13
• Sign formula for the Artin symbol of (α) ArtinL.Abelian.apply_artinSymbol_eq_prod_sign_of_sub_one_mem_conductor_u0 297 below · cited by 1 · depth 14
• Inflation invariance of conductor, local values and plus places ArtinL.Abelian.conductor_comp_restrictNormalHom 16 below · cited by 1 · depth 14
• Primes dividing the Artin conductor are exactly the ramified ones ArtinL.Abelian.dvd_conductor_iff_not_isUnramifiedAt 0 below · cited by 2 · depth 14
• Minimality of the conductor of an abelian character ArtinL.Abelian.exists_apply_artinSymbol_ne_one_of_conductor_lt_u0 322 below · cited by 1 · depth 14
• p-adic valuation of the norm of the abelian conductor ArtinL.Abelian.factorization_absNorm_conductor_eq_finsum_inertiaDeg_mul_conductorExponent 0 below · cited by 1 · depth 14
• Character sum over lower ramification groups at Q ArtinL.Abelian.finsum_sum_one_sub_apply_inertia_pow_eq_ramificationIdx_mul_conductorExponent 25 below · cited by 1 · depth 14
• Averaging an induced character over inertia at p ArtinL.Abelian.inv_card_inertia_mul_sum_induced_frob_pow_mul_eq_finsum 2 below · cited by 1 · depth 14
• Characters annihilate Artin symbols of totally positive α≡1 mod conductor ArtinL.Abelian.apply_artinSymbol_eq_one_of_sub_one_mem_conductor_u0 296 below · cited by 2 · depth 15
• Minimality half of the local conductor exponent at v ArtinL.Abelian.exists_apply_artinSymbol_ne_one_of_one_le_conductorExponent_u0 314 below · cited by 1 · depth 15
• Inertia groups at conjugate primes are conjugate ArtinL.Abelian.exists_inertia_pow_eq_map_conj_ramificationGroup_of_under_eq 0 below · cited by 2 · depth 15
• Artin's dictionary for primes above p modulo H ArtinL.Abelian.galois_primesOver_dictionary 0 below · cited by 1 · depth 15
• Unramifiedness and local value for a character of H ArtinL.Abelian.isUnramifiedAt_ofSubgroup_iff_and_localValue_eq 0 below · cited by 1 · depth 15
• Hasse–Arf: integrality of the Swan conductor of ψ ArtinL.Abelian.natCeil_swanConductor_eq 23 below · cited by 2 · depth 15
• Inflation invariance of the Swan conductor (Herbrand) ArtinL.Abelian.swanConductor_comp_restrictNormalHom 15 below · cited by 1 · depth 15
• Triviality of ψ on Artin symbols above the conductor exponent ArtinL.Abelian.apply_artinSymbol_eq_one_of_sub_one_mem_pow_mul_of_conductorExponent_le_u0 292 below · cited by 1 · depth 16
• Characters annihilating r on congruent unit idèles ArtinL.Abelian.apply_idelicArtinMap_eq_one_of_isAdjuster_of_forall_valued_eq_one 2 below · cited by 2 · depth 16
• Upper ramification jumps versus Swan conductor of ψ ArtinL.Abelian.forall_mem_upperRamificationGroup_apply_eq_one_iff_swanConductor_lt 2 below · cited by 1 · depth 16
• Characters kill upper ramification groups above the conductor exponent ArtinL.Abelian.forall_mem_upperRamificationGroup_apply_eq_one_of_conductorExponent_le 2 below · cited by 2 · depth 17