← all areas

Namespace NumberField 766 theorems

— 154 · AdeleRing 31 · AdelicBox 17 · AdelicFourier 65 · AdelicHaar 11 · AdelicHeight 14 · AdelicLevel 17 · AdelicTrace 1 · AdicCompletion 6 · ArchIdele 3 · FinitePlace 2 · FiniteSIdele 6 · Idele 37 · IdeleClassGroup 10 · IdeleLocalInv 11 · InfPlaceDecomp 12 · InfiniteAdeleRing 15 · InfinitePlace 10 · InfinitePlaceTransport 4 · LevelArith 85 · NormIndex 2 · PlaceDecomp 71 · PlaceTransport 11 · PrimeNormIndex 7 · QuadraticNormIndex 1 · SArchIdele 3 · SIdele 11 · SUnits 14 · StandardAddChar 10 · TateGlobal 96 · Units 2 · mixedEmbedding 27

directly in NumberField 154

• Lifting inertia from a finite Galois subfield to G_ℚ NumberField.exists_lift_mem_inertia_integralClosure 0 below · cited by 7 · depth 8
• Inertia subgroups generate Gal(K/ℚ) NumberField.subgroup_eq_top_of_forall_inertia_le 0 below · cited by 1 · depth 8
• Non-split degree-one primes generate the class group NumberField.classGroup_eq_closure_nonSplit_degOne 2 below · cited by 1 · depth 9
• Subgroups containing all ℚ(ζ₃)-inertia contain Stab(ζ₃) NumberField.stabilizer_primitiveRoot_three_le_of_forall_inertia_inf_le 1 below · cited by 1 · depth 9
• Discriminant bound 3⁹⁵ for degree-48 fields unramified outside 3 NumberField.abs_discr_le_three_pow_95_of_isGalois_of_finrank_eq_48 1 below · cited by 1 · depth 10
• Counting ideals in a fixed class, with power saving NumberField.exists_isBigO_card_absNorm_le_mk_eq_sub 0 below · cited by 1 · depth 10
• Lifting the arithmetic Frobenius at Q to Gal(ℚ̄/ℚ) NumberField.exists_isFrobenius_lift_arithFrobAt 0 below · cited by 5 · depth 10
• Localisation of ℤ̄ at a maximal ideal is a valuation subring NumberField.exists_valuationSubring_eq_localization 0 below · cited by 5 · depth 10
• ℚ(ζ₃) has no unramified nontrivial extension NumberField.finrank_cyclotomicField_three_eq_one_of_forall_isUnramifiedAt 0 below · cited by 1 · depth 10
• Odlyzko bound: root discriminant ≥ 9.805 in degree ≥ 24 NumberField.odlyzko_bound_9805_of_isTotallyComplex_of_twentyfour_le_finrank 4 below · cited by 1 · depth 10
• Split primes bounded by q⁻¹logζ_M(s) NumberField.tsum_split_degOne_le 0 below · cited by 1 · depth 10
• Odlyzko's explicit-formula discriminant bound, totally complex case NumberField.archTermDerived_le_log_abs_discr 2 below · cited by 1 · depth 11
• Different exponent at a prime above 3 is at most e+e v₃(e)-1 NumberField.count_normalizedFactors_differentIdeal_le_of_mem_primesOverFinset_three 0 below · cited by 1 · depth 11
• Galois extensions of ℚ unramified outside 3 of 2-power degree NumberField.finrank_le_two_of_isGalois_of_isUnramifiedAt_of_finrank_dvd_sixteen 0 below · cited by 1 · depth 11
• Completed Dedekind zeta: continuation, functional equation, growth NumberField.exists_completedDedekindZeta_package 0 below · cited by 10 · depth 12
• Hadamard expansion of ξ_K'/ξ_K over critical-strip zeros NumberField.exists_hadamard_logDeriv_expansion_of_completedZeta_package 0 below · cited by 1 · depth 12
• Chebotarev existence: every Galois element is an arithmetic Frobenius NumberField.exists_prime_isArithFrobAt_of_isGalois 13 below · cited by 1 · depth 12
• Hecke's functional equation for primitive narrow ray class characters NumberField.exists_completedRayL_functionalEquation_of_primitive 4 below · cited by 1 · depth 13
• Arithmetic Frobenius realising any automorphism of a cyclotomic extension NumberField.exists_prime_isArithFrobAt_of_isCyclotomicExtension 12 below · cited by 1 · depth 13
• Summability of (N𝔭)^{-σ} over primes for σ>1 NumberField.summable_heightOneSpectrum_absNorm_rpow_neg_of_one_lt 0 below · cited by 41 · depth 13
• Discriminant of a fixed field from ramification filtrations at p NumberField.card_mul_factorization_discr_fixedField_eq_inertiaDeg_mul_finsum_u0 9 below · cited by 3 · depth 14
• Hecke's functional equation for narrow class characters NumberField.exists_completedRayL_functionalEquation_of_modulus_top 0 below · cited by 1 · depth 14
• Existence of a Gauss datum for a narrow ray class character NumberField.exists_isGaussDatum 0 below · cited by 1 · depth 14
• Prescribed signs for integers congruent to 1 mod 𝔪 NumberField.exists_ne_zero_and_sub_one_mem_and_lt_zero_iff 0 below · cited by 8 · depth 14
• Primes of absolute degree one realising a cyclotomic automorphism NumberField.exists_prime_absNorm_eq_and_apply_eq_pow_of_isCyclotomicExtension 11 below · cited by 1 · depth 14
• Archimedean signs of a narrow ray class symbol NumberField.exists_sq_eq_one_and_raySymbol_span_singleton_eq_prod_of_forall_pos 1 below · cited by 1 · depth 14
• Weak approximation: K dense in prod_{v∈ S}Kᵥ×prod_{w∣∞}K_w NumberField.denseRange_algebraMap_adicCompletion_pi_prod_infinitePlace_pi 1 below · cited by 5 · depth 15
• Artin symbol of a principal ideal congruent to 1 NumberField.exists_artinSymbol_principalUnit_eq_prod_of_isConj 118 below · cited by 4 · depth 15
• Divergence of prime sums in a norm class mod m NumberField.exists_forall_le_tsum_absNorm_rpow_neg_of_isCyclotomicExtension 10 below · cited by 1 · depth 15
• Sign of a relative norm at a real embedding NumberField.apply_norm_lt_zero_iff_odd_card_filter 0 below · cited by 1 · depth 16
• Logarithm of a narrow ray class L-series as a prime sum NumberField.exists_continuousOn_exp_eq_rayClassLSeries 0 below · cited by 2 · depth 16
• Entireness of non-trivial narrow ray class L-series (Hecke) NumberField.exists_differentiable_eq_rayClassLSeries_of_ne_one 1 below · cited by 2 · depth 16
• Places above an unramified place as Frobenius orbits on cosets NumberField.exists_equiv_under_eq_orbitRel_quotient_zpowers_forall_inertiaDeg_eq_card_orbit 0 below · cited by 1 · depth 16
• A prime outside a finite set, unramified with a degree-one place NumberField.exists_heightOneSpectrum_notMem_and_extension_ne_and_inertiaDeg_eq_one_and_ramificationIdx_eq_one 6 below · cited by 2 · depth 16
• Idelic Artin map for an admissible modulus of the degree NumberField.exists_idelicArtinMap_ker_eq_and_surjective_and_eq_finprod_artinFrob_of_isAdmissibleModulusOfDegree_finrank 132 below · cited by 17 · depth 16
• An everywhere-unramified number field is ℚ NumberField.finrank_eq_one_of_forall_isUnramifiedAt 0 below · cited by 1 · depth 16
• Primes with norm ≡ 1 (mod m) split completely in K(ζ_m) NumberField.ncard_primesOver_eq_finrank_of_isCyclotomicExtension_of_absNorm_modEq_one 0 below · cited by 2 · depth 16
• Artin symbol of a principal ideal on roots of unity NumberField.raySymbol_artinFrob_apply_eq_pow_absNorm_of_pow_eq_one 0 below · cited by 1 · depth 16
• Chebotarev lower bound for arithmetic Frobenius, Dirichlet form NumberField.sub_mul_log_le_tsum_ncard_isArithFrobAt 12 below · cited by 1 · depth 16
• Integral Galois orthogonality relations in a number field NumberField.exists_isIntegral_discr_mul_and_sum_algEquiv_apply_mul_eq 0 below · cited by 1 · depth 17
• Euler product for the Dedekind zeta function NumberField.hasProd_inv_one_sub_absNorm_cpow_neg_dedekindZeta 0 below · cited by 26 · depth 17
• Restriction maps inertia into inertia in a tower NumberField.map_restrictNormalHom_inertia_le_inertia_under 0 below · cited by 1 · depth 17
• Dirichlet-density lower bound for Frobenius primes in K(ζ_m)/K NumberField.sub_mul_log_le_tsum_ncard_isArithFrobAt_of_isCyclotomicExtension 11 below · cited by 1 · depth 17
• Density of K in its finite adèles, with ring-map rigidity NumberField.denseRange_algebraMap_finiteAdeleRing_and_ringHom_ext 0 below · cited by 3 · depth 18
• Partial Dedekind zeta function: continuation and simple pole at s=1 NumberField.exists_differentiableOn_eq_tprod_inv_one_sub_absNorm_cpow_neg_and_tendsto_sub_one_mul 1 below · cited by 2 · depth 18
• Hecke's density theorem for prime norms in a residue class NumberField.exists_forall_abs_tsum_absNorm_rpow_neg_sub_inv_finrank_mul_log_le_of_isCyclotomicExtension 10 below · cited by 1 · depth 18
• Idelic reciprocity map for abelian extensions of exponent dividing 24 NumberField.exists_idelicArtinMap_ker_eq_and_surjective_and_eq_finprod_artinFrob_of_dvd_twentyFour 130 below · cited by 1 · depth 18
• Finite places of number fields extend to ℚ̄ NumberField.exists_isNonarchimedean_absoluteValue_extends 0 below · cited by 3 · depth 18
• Local p-th powers away from S ∪ T are global NumberField.exists_pow_eq_of_forall_mem_range_powMonoidHom 66 below · cited by 2 · depth 18
• Convergence, holomorphy and non-vanishing of degree-one Euler products NumberField.multipliable_differentiableOn_tprod_ne_zero_eulerProduct_of_norm_le_one 0 below · cited by 40 · depth 18
• Order of U_S/U_Sⁿ when μₙ ⊆ K NumberField.natCard_sUnit_quotient_range_powMonoidHom 3 below · cited by 2 · depth 18
• No vanishing of Euler products at σdownarrow 1 NumberField.not_tendsto_tprod_eulerProduct_nhdsGT_one_nhds_zero_of_three_four_one 0 below · cited by 1 · depth 18
• Completed fundamental identity: prod_{v∈ S}#(mathcal Oᵥ/pmathcal Oᵥ)=p^{[K:ℚ]} NumberField.prod_natCard_adicCompletionIntegers_quotient_span_natCast_eq_pow_finrank 1 below · cited by 2 · depth 18
• Product of local p-th power indices over S and ∞ NumberField.prod_natCard_units_adicCompletion_quotient_range_powMonoidHom_mul_prod_infinitePlace_eq_pow 17 below · cited by 2 · depth 18
• Divergence at s=1⁺ of the Euler product off a finite set NumberField.tendsto_norm_tprod_inv_one_sub_absNorm_cpow_neg_nhdsGT_one_atTop 0 below · cited by 1 · depth 18
• Strong approximation: SL₂(F) dense in SL₂(A_F^f) NumberField.denseRange_specialLinearGroup_map_finiteAdeleRing 0 below · cited by 1 · depth 19
• Entirety of (s-1)ζ_K(s) and its trivial zeros NumberField.exists_differentiable_eq_sub_one_mul_dedekindZeta_and_apply_neg_two_mul_add_one_eq_zero 1 below · cited by 18 · depth 19
• Finite extensions of number fields are unramified outside a finite set NumberField.exists_finset_forall_ramificationIdx_eq_one 1 below · cited by 4 · depth 19
• p-capitulation of S-idèle classes at a Galois level NumberField.exists_le_isGalois_forall_mem_range_sup_unitIdelesOutside_of_pow_mem 13 below · cited by 3 · depth 19
• Euler product for a restricted Dedekind zeta function NumberField.hasProd_inv_one_sub_absNorm_cpow_neg_lSeries_card_ideal_of_forall_dvd 0 below · cited by 1 · depth 19
• Index of n-th powers in Kᵥ^× when μₙ ⊆ Kᵥ NumberField.natCard_units_adicCompletion_quotient_range_powMonoidHom 13 below · cited by 1 · depth 19
• Trivial inertia above ℓ implies e(Q∣ℓ)=1 NumberField.ramificationIdx_span_eq_one_of_forall_liesOverPrime_inertiaSubgroupIn_le_fixingSubgroup 2 below · cited by 3 · depth 19
• Non-vanishing of ζ_K on Re(s)>1 NumberField.dedekindZeta_ne_zero_of_one_lt_re 0 below · cited by 6 · depth 20
• Weak approximation at the infinite places and a finite set S NumberField.denseRange_algebraMap_infiniteAdeleRing_prod_adicCompletion 0 below · cited by 1 · depth 20
• The discriminant sign character of a number field NumberField.exists_isAdmissibleTwist_mul_self_eq_one_and_isUnramifiedCharAt_and_apply_uniformizerIdele_eq_neg_one_pow_of_not_isRamifiedIn 264 below · cited by 1 · depth 20
• Existence of a Galois compositum of two Galois number fields NumberField.exists_isGalois_compositum 0 below · cited by 5 · depth 20
• Abelian cyclotomic layer, unramified at v with local degree divisible by n NumberField.exists_isMulCommutative_algHom_cyclotomicField_ramificationIdx_eq_one_and_dvd_natCard_decomp 1 below · cited by 1 · depth 20
• Capitulation of p-power classes in a Galois level unramified outside S NumberField.exists_le_isGalois_forall_classGroup_map_eq_one_of_pow_eq_one 9 below · cited by 1 · depth 20
• Finite primes of subfields of ℚ̄ lift to valuation subrings NumberField.exists_valuationSubring_algebraicClosure_forall_mem_iff_valuation_le_one 4 below · cited by 4 · depth 20
• Index of n-th powers in local units when μₙ ⊆ Kᵥ NumberField.natCard_units_adicCompletionIntegers_quotient_range_powMonoidHom 11 below · cited by 1 · depth 20
• Continuous map K_w → ℚ̄_q forces residue characteristic q NumberField.natCast_mem_asIdeal_of_continuous_ringHom_adicCompletion_padicAlgCl 0 below · cited by 2 · depth 20
• Trivial inertia above ℓ forces e(Q∣ Q∩𝒪_K)=1 NumberField.ramificationIdx_under_eq_one_of_forall_liesOverPrime_inertiaSubgroupIn_le_fixingSubgroup 2 below · cited by 6 · depth 20
• Finiteness of the Dedekind zeta series at real t>1 NumberField.tsum_prod_absNorm_heightOneSpectrum_pow_rpow_neg_lt_top 0 below · cited by 5 · depth 20
• Additive strong approximation away from one finite place NumberField.denseRange_algebraMap_add_adeleSingleAt 0 below · cited by 1 · depth 21
• Valuation subrings of Ω pulled back along K → Ω give primes NumberField.existsUnique_heightOneSpectrum_forall_map_mem_iff_valuation_le_one 1 below · cited by 10 · depth 21
• Artin's lemma on cyclic cyclotomic extensions with prescribed local degrees NumberField.exists_isCyclic_algHom_cyclotomicField_dvd_natCard_decomp 8 below · cited by 2 · depth 21
• Ternary quadratic form represents every non-square locally NumberField.exists_ternary_quadratic_eq_adicCompletion_of_not_isSquare 10 below · cited by 1 · depth 21
• Finite primes of a number field extend to places of ℚ̄ NumberField.exists_valuationSubring_forall_map_mem_iff_valuation_le_one 3 below · cited by 3 · depth 21
• Sign character subextension: degree ≤ 2 and inertia degree via Frobenius NumberField.finrank_fixedField_ker_sign_le_two_and_inertiaDeg_iff_of_isArithFrobAt 0 below · cited by 2 · depth 21
• Unramified primes stay unramified in the normal closure NumberField.ramificationIdxIn_eq_one_of_isNormalClosure_of_forall_ramificationIdx_eq_one 0 below · cited by 2 · depth 21
• Sign of Frobenius on G/H is (-1)^{[K:E]+rᵥ} NumberField.sign_toPerm_quotient_fixingSubgroup_fieldRange_eq_neg_one_pow_of_isArithFrobAt 1 below · cited by 2 · depth 21
• Compositum of a Galois p-extension with a cyclic extension of equal degree NumberField.compositum_isPGroup_and_normal_and_inf_eq_bot_and_exists_generators 0 below · cited by 2 · depth 22
• Compositum coordinates for a Galois and a cyclic layer NumberField.compositum_normal_and_inf_eq_bot_and_exists_generators 0 below · cited by 1 · depth 22
• Frobenius orbits on cosets match primes above v NumberField.exists_equiv_orbitRel_zpowers_quotient_fixingSubgroup_primeFibre_of_isArithFrobAt 0 below · cited by 1 · depth 22
• Adelic bound for dilation-dominated equivariant families on A_F^× NumberField.exists_isCompact_forall_tsum_le_mul_rpow_neg_of_principal_equivariant_of_dilation_bound 8 below · cited by 3 · depth 22
• Compositum of coprime cyclic cyclotomic layers with prescribed local degrees NumberField.exists_isCyclic_algHom_cyclotomicField_mul_dvd_natCard_decomp_of_coprime 3 below · cited by 1 · depth 22
• Cyclic p-power subfield of E(ζ_{p^k}) with large local degrees NumberField.exists_isCyclic_algHom_cyclotomicField_pow_dvd_natCard_decomp 5 below · cited by 3 · depth 22
• Existence of cyclic extensions of prescribed degree NumberField.exists_isCyclic_finrank_eq 9 below · cited by 1 · depth 22
• Sums over finite places as a Dirichlet series, abscissa ≤ 2 NumberField.exists_nonneg_abscissa_le_hasSum_tsum_mul_absNorm_cpow_eq_lseries_of_le_mul_pow 1 below · cited by 1 · depth 22
• Galois group of a compositum of p-extensions is a p-group NumberField.isPGroup_algEquiv_compositum_of_isPGroup 0 below · cited by 1 · depth 22
• Hasse norm theorem for cyclic extensions NumberField.exists_algebraNorm_eq_of_mem_range_idelicNorm_of_isCyclic 122 below · cited by 7 · depth 23
• p^N divides degree and local degrees of deep cyclotomic layers NumberField.exists_forall_pow_dvd_natCard_decomp_cyclotomicField_and_dvd_natCard_algEquiv 1 below · cited by 1 · depth 23
• Cyclic cyclotomic extensions of prescribed p-power degree NumberField.exists_intermediateField_cyclotomicField_isCyclic_finrank_eq_pow 0 below · cited by 1 · depth 23
• Quadratic sign character with conductor bounded by d_K NumberField.exists_isAdmissibleTwist_mul_self_eq_one_and_apply_uniformizerIdele_eq_neg_one_pow_and_localChar_eq_one_of_factorization_discr_le 306 below · cited by 1 · depth 23
• Norm group of the Kummer extension by p-th roots of S'-units NumberField.exists_isGalois_principalIdeles_sup_range_idelicNorm_eq_unitIdelesTrivialOn_of_sup_unitIdelesOutside_eq_top 144 below · cited by 1 · depth 23
• Degree, kernel and ramification for the field cut out by H₀ NumberField.finrank_eq_index_and_ker_eq_and_ramificationIdx_eq_one_of_restrictNormalHom_ker_eq_map 0 below · cited by 1 · depth 23
• Discriminant exponent as inertia-weighted sum of character levels NumberField.natCast_factorization_natAbs_discr_eq_finsum_inertiaDeg_mul_addCharLevel_psiLocal 10 below · cited by 1 · depth 23
• The prime attached to an embedding and place divides p NumberField.natCast_mem_asIdeal_of_forall_map_mem_iff_valuation_le_one 0 below · cited by 2 · depth 23
• Base-changed idèles become norms after raising to n'/[F:E] NumberField.pow_map_genuineBaseChange_mem_principalIdeles_sup_range_idelicNorm 144 below · cited by 1 · depth 23
• Everywhere-local norms give an idelic norm NumberField.unitsMap_algebraMap_mem_range_idelicNorm_of_forall_exists_norm_eq 6 below · cited by 3 · depth 23
• Discriminant of the quadratic resolvent divides d_K NumberField.discr_fixedField_ker_sign_comp_toPermHom_quotient_fixingSubgroup_dvd_discr 10 below · cited by 1 · depth 24
• Idelic Artin map for a modulus whose unit idèles are norms NumberField.exists_idelicArtinMap_ker_eq_and_surjective_and_eq_finprod_artinFrob_of_unitIdeles_le 135 below · cited by 2 · depth 24
• Partial Dedekind zeta function: continuation, Euler product, simple pole NumberField.exists_meromorphicOn_mul_tprod_one_sub_absNorm_cpow_neg_eq_one_and_tendsto_sub_one_mul 1 below · cited by 2 · depth 24
• Fibre integration of the idelic norm over a fundamental domain NumberField.exists_setLIntegral_comp_idelicNorm_eq_mul_and_setIntegral_comp_idelicNorm_eq_mul 23 below · cited by 2 · depth 24
• Vanishing of ̂ H⁻¹(G,C_L) for cyclic L/K NumberField.ideleClassNorm_ker_eq_ideleClassDerive_range 120 below · cited by 1 · depth 24
• Compactness of norm-one ideles modulo σ(w)/w NumberField.exists_isCompact_ker_idelicNorm_subset_range_mul_of_forall_mem_zpowers 8 below · cited by 1 · depth 25
• Norm-coset index in the ideles divides [L:K] NumberField.ideleClass_normCoset_index_dvd_finrank 117 below · cited by 2 · depth 25
• Sum of base-change characters against a test function, given κ NumberField.sum_integral_mul_eq_mul_finsum_setIntegral_comp_idelicNorm_of_setIntegral_comp_idelicNorm_eq_mul 219 below · cited by 1 · depth 25
• Idelic norm preserves the adelic modulus NumberField.distribHaarChar_idelicNorm_genuineBaseChange 0 below · cited by 5 · depth 26
• Characters above ξ_L as integrals over norm fibres NumberField.exists_sum_integral_mul_eq_mul_finsum_setIntegral_comp_idelicNorm_of_isFundamentalDomain 231 below · cited by 1 · depth 26
• Summing G over cosets of the idelic norm group NumberField.finsum_setIntegral_range_idelicNorm_comp_mul_eq_setIntegral_principalIdeles_sup_range_of_prime 125 below · cited by 1 · depth 26
• Openness of the idelic norm group N(A_L^×) NumberField.isOpen_range_idelicNorm 9 below · cited by 9 · depth 26
• Openness of n-th powers in Kᵥ^× NumberField.isOpen_range_powMonoidHom_units_adicCompletion 2 below · cited by 2 · depth 26
• Vanishing of a character integral against functions of the idelic norm NumberField.setIntegral_ideleChar_mul_comp_idelicNorm_eq_zero_of_exists_idelicNorm_eq_one 0 below · cited by 2 · depth 26
• Sums over idele class characters of K lying above ξ_L NumberField.sum_ideleClassChar_eq_of_comp_idelicNorm_eq 10 below · cited by 3 · depth 26
• A summable majorant over the finite places of ℚ NumberField.summable_heightOneSpectrum_tsum_pow_mul_absNorm_rpow_neg_rat 1 below · cited by 1 · depth 27
• A diag(varpi,1) Hecke coset system has N(w)+1 members NumberField.eq_absNorm_add_one_of_isHeckeCosetSystem_diagPi 0 below · cited by 2 · depth 29
• Finitely many unit-character restrictions at bounded level NumberField.exists_finite_forall_localFamily_eq_on_units_of_trivial_on_congruenceUnits 0 below · cited by 1 · depth 29
• Even number of places where a fails to be a local norm NumberField.finite_and_even_ncard_places_not_mem_range_norm_of_finrank_eq_two 269 below · cited by 2 · depth 29
• Uniform count of 2π-integral vectors of bounded spread modulo units NumberField.exists_forall_finite_and_ncard_setOf_sum_mult_mul_sub_mul_log_unit_le_mul_one_add_pow 1 below · cited by 1 · depth 30
• Polynomial bound for (s-1)ζ_K(s) on Re s=-1/2 NumberField.exists_forall_norm_sub_one_mul_dedekindZeta_continuation_le_rpow_on_re_eq_neg_half 4 below · cited by 1 · depth 30
• Quadratic idele class character of a quadratic extension NumberField.exists_isIdeleClassChar_ne_one_localChar_eq_one_of_mem_range_norm_of_finrank_eq_two 136 below · cited by 1 · depth 30
• Gaussian growth bound for (s-1)ζ_K(s) in vertical strips NumberField.exists_norm_sub_one_mul_dedekindZeta_continuation_le_mul_exp_mul_im_sq 1 below · cited by 1 · depth 30
• Fibre integration for the idelic norm on A_L^×/N¹ NumberField.exists_pos_forall_lintegral_comp_idelicNorm_haarQuotient_ker_eq_mul_setLIntegral_range 18 below · cited by 3 · depth 30
• Local norm index divides 2 in a quadratic extension NumberField.index_range_norm_dvd_two_of_finrank_eq_two 7 below · cited by 1 · depth 30
• Local components of an idele class character at non-norm places NumberField.localChar_ne_one_of_range_norm_ne_top_of_isIdeleClassChar_of_finrank_eq_two 264 below · cited by 1 · depth 30
• Vanishing of int_Ω ξ F when ξ(t)≠ 1 NumberField.setIntegral_ideleClassChar_mul_eq_zero_of_isFundamentalDomain_of_forall_mul_eq_of_apply_ne_one 0 below · cited by 4 · depth 30
• Changing the excluded set in a degree-one Euler product NumberField.tprod_inv_eulerFactor_mul_tprod_eulerFactor_eq_prod_sdiff_of_norm_le_one 1 below · cited by 1 · depth 30
• Adelic decay of principal-equivariant families with archimedean dilation bound NumberField.exists_isCompact_forall_tsum_le_mul_rpow_neg_of_principal_equivariant_of_dilation_bound_of_rpow_inv_le 8 below · cited by 2 · depth 31
• Local ideles escaping the norm class group in degree two NumberField.exists_localIdele_not_mem_principalIdeles_sup_range_idelicNorm_of_finrank_eq_two 260 below · cited by 1 · depth 31
• Orthogonality of idele class characters above ξ_L NumberField.sum_apply_eq_zero_of_not_mem_principalIdeles_sup_range_idelicNorm_and_sum_apply_mul_idelicNorm_eq_card_mul 10 below · cited by 1 · depth 31
• Summing int ξ F over characters above ξ_L via the norm fibration NumberField.sum_integral_mul_eq_card_div_mul_integral_haarQuotient_ker_idelicNorm_of_forall_eq_zero_of_not_mem_range 0 below · cited by 2 · depth 31
• Positivity of the norm-band constant of a fundamental domain NumberField.toReal_measure_inter_ideleNorm_det_centralScalar_mem_Icc_pos_of_isFundamentalDomain 53 below · cited by 1 · depth 31
• Rescaled T-unit lattice with divisibility condition NumberField.exists_addSubgroup_discreteTopology_units_log_valuation_div_sum_eq_neg_sum_log_pow_mul 1 below · cited by 4 · depth 32
• The T-unit lattice: discreteness, product formula, torsion kernel NumberField.exists_addSubgroup_discreteTopology_units_log_valuation_sum_eq_neg_sum_log_absNorm_mul 0 below · cited by 7 · depth 32
• Hyperbolic class sums as finitely many twisted lattice sums NumberField.exists_addSubgroup_forall_finsum_units_mul_prod_zpow_neg_mul_sum_integral_window_eq_sum_tsum_ite_of_contDiff_of_isLocallyConstant 31 below · cited by 1 · depth 32
• Artin symbol nontrivial at a ramified real place NumberField.exists_artinSymbol_principalUnit_ne_one_of_not_isReal 119 below · cited by 1 · depth 32
• Torsion-free complement of the T-units, with finite local-sign classes NumberField.exists_subgroup_units_valuationOfNeZero_eq_one_inf_torsion_eq_bot_existsUnique_coset_of_isOpen 2 below · cited by 4 · depth 32
• Embedding of L into Kᵥ at a split place NumberField.nonempty_algHom_adicCompletion_of_nontrivial_extension_of_prime 1 below · cited by 2 · depth 32
• Product formula over any sufficiently large finite set of primes NumberField.exists_finset_forall_prod_infinitePlace_pow_mul_prod_norm_algebraMap_adicCompletion_eq_one 0 below · cited by 2 · depth 33
• Counting elements of K with bounded S-adic and archimedean logs NumberField.exists_forall_card_le_mul_prod_of_forall_norm_eq_one_of_abs_log_norm_le 1 below · cited by 1 · depth 33
• Uniform quotient-measure bound for squared idelic norm preimages NumberField.exists_forall_haarQuotient_ker_idelicNorm_setOf_idelicNorm_sq_mul_mem_le 20 below · cited by 1 · depth 33
• Non-norms at exactly one place are impossible (prime cyclic degree) NumberField.finite_and_ncard_places_not_mem_range_norm_add_ne_one_of_forall_mem_zpowers_of_prime 281 below · cited by 2 · depth 33
• Covolume of the principal norm-one ideles in a cyclic extension NumberField.measure_fundamentalDomain_range_div_eq_mul_finrank_mul_div_of_ker_idelicNorm 27 below · cited by 1 · depth 33
• From a Γ-fundamental domain to the norm-one idele quotient NumberField.setLIntegral_comp_idelicNorm_fundamentalDomain_eq_measure_mul_lintegral_haarQuotient_ker 4 below · cited by 1 · depth 33
• Transport of a fundamental domain along idelic Hilbert 90 NumberField.ae_exists_mk_mul_out_mem_and_measure_inter_eq_zero_preimage_unitsAct_mul_inv_of_isFundamentalDomain_subgroupOf 3 below · cited by 1 · depth 34
• Discrepancy-window class sums as summable lattice sums of kink windows NumberField.exists_addSubgroup_forall_finsum_units_mul_prod_zpow_neg_mul_sum_integral_discWindow_eq_tsum_mul_tsum_ite_kinkWindow_of_contDiff_of_forall_eq_of_norm_sub_le 42 below · cited by 1 · depth 34
• Uniform finiteness of elements with prescribed valuations and bounded archimedean sizes NumberField.exists_forall_finite_and_ncard_le_setOf_forall_valuation_eq_of_forall_apply_mem_Icc 0 below · cited by 1 · depth 34
• Covolume of L^×/K^× in A_L^×/A_K^× NumberField.haarQuotient_measure_eq_ofReal_finrank_mul_div_of_ae_exists_mk_mul_out_mem_of_measure_inter_eq_zero 23 below · cited by 1 · depth 34
• Euler product and residue at s=1 of ζ_K(2s)ζ_K(2s-1) NumberField.hasProd_and_tendsto_sub_one_mul_dedekindZeta_two_mul_mul_dedekindZeta_two_mul_sub_one_nhdsGT 3 below · cited by 2 · depth 34
• Adelic height bound from a factorised identity (1-c)x=sumⱼ PⱼUⱼ NumberField.sum_mult_mul_log_one_add_norm_sq_add_two_mul_finsum_log_max_norm_le_of_one_sub_mul_eq_sum 1 below · cited by 1 · depth 34
• Euler product and residue of ζ_K(2s)ζ_K(2s-1) in [0,∞] NumberField.tendsto_prod_sdiff_inv_one_sub_absNorm_rpow_atTop_and_tendsto_sub_one_mul_re_dedekindZeta_two_mul_nhdsGT 4 below · cited by 1 · depth 34
• Places bound: total smallness of 1-c versus size of c NumberField.finsum_posLog_inv_norm_one_sub_add_sum_mult_mul_posLog_inv_le 0 below · cited by 1 · depth 35
• Inertia field is unramified; all ramification lies above it NumberField.ramificationIdx_under_fixedField_inertia_eq_one 0 below · cited by 1 · depth 35

NumberField.AdeleRing 31

• Adelic modulus of a principal idele is 1 NumberField.AdeleRing.distribHaarChar_algebraMap 2 below · cited by 150 · depth 16
• Modulus of an idele as a product of local norms NumberField.AdeleRing.distribHaarChar_eq_prod_norm_pow_mult_mul_finprod_norm 1 below · cited by 77 · depth 16
• Modulus of an idele with trivial finite part NumberField.AdeleRing.distribHaarChar_eq_prod_norm_pow_mult_of_snd_eq_one 0 below · cited by 33 · depth 16
• Finitely many principal adeles in a compact set NumberField.AdeleRing.finite_setOf_algebraMap_mem_of_isCompact 0 below · cited by 41 · depth 16
• Unit idèles outside T characterised by valuations NumberField.AdeleRing.mem_unitIdelesOutside_iff_forall_valued_snd_eq_one 0 below · cited by 6 · depth 16
• Compactness of the adele class group A_F/F NumberField.AdeleRing.compactSpace_quotient_principalSubgroup 0 below · cited by 3 · depth 17
• Quantitative count of field elements in an adelic box NumberField.AdeleRing.exists_finset_forall_mem_and_card_le_mul_prod_pow_of_isCompact 1 below · cited by 3 · depth 17
• Discreteness of the principal ideles in the idele group NumberField.AdeleRing.exists_isOpen_inter_principalIdeles_eq_singleton 0 below · cited by 4 · depth 17
• Multiplication by a principal adele preserves additive Haar measure NumberField.AdeleRing.measurePreserving_mul_algebraMap 1 below · cited by 2 · depth 17
• Second countability of the adele ring of a number field NumberField.AdeleRing.secondCountableTopology 0 below · cited by 265 · depth 17
• Principal idèles in the S-unit idèles are the S-units NumberField.AdeleRing.principalIdeles_inf_unitIdelesOutside_eq_map_unit 0 below · cited by 5 · depth 18
• Every idele is principal times an S-unit idele NumberField.AdeleRing.principalIdeles_sup_unitIdelesOutside_eq_top 1 below · cited by 2 · depth 18
• Index of an idèle box in the S-unit idèles NumberField.AdeleRing.relIndex_ideleBox_unitIdelesOutside 0 below · cited by 2 · depth 18
• GL₂ of the adeles is second countable NumberField.AdeleRing.secondCountableTopology_generalLinearGroup_finTwo 1 below · cited by 217 · depth 18
• Finite index of principal times S-unit idèles NumberField.AdeleRing.finiteIndex_principalIdeles_sup_unitIdelesOutside 1 below · cited by 5 · depth 19
• Principal idèles and an idèle box exhaust the idèle group NumberField.AdeleRing.principalIdeles_sup_ideleBox_eq_top 0 below · cited by 1 · depth 19
• Index p^{2(|S|+r₁+r₂)} of the local p-th power idèle box NumberField.AdeleRing.relIndex_ideleBox_range_powMonoidHom_unitIdelesOutside_eq_pow 19 below · cited by 1 · depth 24
• Idèle cocycles modulo unit idèles outside S are coboundaries NumberField.AdeleRing.exists_forall_mul_inv_smul_div_mem_unitIdelesOutside_of_forall_mem 9 below · cited by 2 · depth 27
• Genuine base change preserves S-unit idèles and S-units NumberField.AdeleRing.unitsMap_genuineBaseChange_mem_unitIdelesOutside_of_isScalarTower 2 below · cited by 1 · depth 27
• An idèle with prescribed valuations at all finite places NumberField.AdeleRing.exists_units_forall_valued_snd_eq_ofAdd_neg 0 below · cited by 2 · depth 28
• An idèle is a local unit at almost all finite places NumberField.AdeleRing.finite_setOf_valued_snd_ne_one 0 below · cited by 2 · depth 28
• Freeness over the adele ring from a free multiple NumberField.AdeleRing.free_of_pi_linearEquiv_pi 0 below · cited by 2 · depth 28
• Squaring is proper on the idele group NumberField.AdeleRing.isCompact_setOf_sq_mem_of_isCompact 0 below · cited by 3 · depth 28
• Galois action on idèles preserves valuations along transported places NumberField.AdeleRing.valued_snd_smul_smul_eq 4 below · cited by 2 · depth 28
• Adeles generating the unit ideal recombine via orthogonal idempotents NumberField.AdeleRing.exists_completeOrthogonalIdempotents_and_isUnit_sum_mul_of_span_range_eq_top 0 below · cited by 1 · depth 29
• Adelic density of everywhere-primitive integral columns NumberField.AdeleRing.dedekindZeta_two_mul_pi_measure_setOf_forall_not_norm_lt_one_eq_pi_measure_setOf_forall_mem_adicCompletionIntegers 4 below · cited by 1 · depth 31
• Compactness of idele boxes with unit components off S NumberField.AdeleRing.isCompact_setOf_units_adeleArch_mem_and_apply_mem_inter_unitIdelesOutside 0 below · cited by 6 · depth 32
• Adelic measure d²c ‖δ‖⁻¹dδ is GL₂-invariant NumberField.AdeleRing.map_mulVec_det_mul_pi_prod_withDensity_ideleNorm_inv_eq_self 3 below · cited by 1 · depth 32
• Almost every adelic pair is a unimodular column NumberField.AdeleRing.pi_measure_setOf_not_exists_apply_col_eq_eq_zero 4 below · cited by 1 · depth 32
• Haar measure on mathbb A_K^ι splits along K_∞^ι×mathbb A_{K,f}^ι NumberField.AdeleRing.exists_isAddHaarMeasure_map_pi_fst_snd_eq_prod 1 below · cited by 3 · depth 34
• The idele group of a number field is Polish NumberField.AdeleRing.polishSpace_units 1 below · cited by 1 · depth 39

NumberField.AdelicBox 17

• Density of 𝒪_F in the integral finite adeles NumberField.AdelicBox.integralFiniteAdeles_subset_closure_range_algebraMap_ringOfIntegers 0 below · cited by 2 · depth 16
• Continuous characters of the finite adeles have a conductor NumberField.AdelicBox.exists_ne_zero_forall_addChar_mul_eq_one 0 below · cited by 3 · depth 17
• Scaling invariance of the adelic box average under F^× NumberField.AdelicBox.integral_cond_adelicBox_comp_mul_algebraMap 3 below · cited by 11 · depth 17
• Dilates of the adelic box are fundamental domains NumberField.AdelicBox.isAddFundamentalDomain_preimage_mul_algebraMap_adelicBox 0 below · cited by 10 · depth 17
• Box-normalised adelic integral of a pure tensor NumberField.AdelicBox.inv_measure_adelicBox_mul_integral_pureTensor_eq 1 below · cited by 6 · depth 19
• Locally constant compactly supported finite-adelic functions span indicator cosets NumberField.AdelicBox.exists_eq_sum_indicator_image_integralFiniteAdeles 0 below · cited by 4 · depth 20
• Affine invariance of adelic box integrals of F-periodic functions NumberField.AdelicBox.setLIntegral_adelicBox_comp_mul_add_eq_of_periodic 3 below · cited by 2 · depth 20
• Principal finite adeles in the coset k + dwidehat𝒪_F NumberField.AdelicBox.algebraMap_mem_image_integralFiniteAdeles_iff 0 below · cited by 3 · depth 22
• Haar measure of the coset k+dwidehat𝒪_F NumberField.AdelicBox.absNorm_mul_measure_image_integralFiniteAdeles 0 below · cited by 2 · depth 23
• Indicator of the coset k+dwidehat𝒪_F is locally constant, compactly supported NumberField.AdelicBox.isLocallyConstant_and_hasCompactSupport_indicator_image_integralFiniteAdeles 0 below · cited by 4 · depth 23
• Bounded denominators on the compact support of a finite-adelic function NumberField.AdelicBox.exists_denom_of_hasCompactSupport 0 below · cited by 1 · depth 24
• Box-indicator decomposition of Schwartz–Bruhat functions on finite adeles NumberField.AdelicBox.exists_eq_sum_indicator_pi_image_integralFiniteAdeles 1 below · cited by 3 · depth 26
• Haar measure on A_F as a scaled product measure NumberField.AdelicBox.map_ringEquiv_mixedSpace_eq_smul_volume_prod 2 below · cited by 5 · depth 26
• Existence of a Haar measure giving the adelic box measure one NumberField.AdelicBox.exists_isAddHaarMeasure_adelicBox_eq_one 0 below · cited by 3 · depth 28
• Unfolding an integrable function over the adelic box NumberField.AdelicBox.setIntegral_adelicBox_tsum_add_algebraMap 0 below · cited by 5 · depth 29
• Adelic box has measure 2^{-r₂}√|d_K| times unit cube NumberField.AdelicBox.measure_adelicBox_eq_measure_unitCubeBox_mul_inv_two_pow_mul_sqrt_discr 3 below · cited by 2 · depth 30
• Adelic Haar measure factorises on pure tensors in two variables NumberField.AdelicBox.lintegral_pi_pureTensor_two_eq_sq_mul_lintegral_pi_volume_mul_lintegral_pi 3 below · cited by 1 · depth 32

NumberField.AdelicFourier 65

• Global additive characters of A_F are unitary NumberField.AdelicFourier.norm_apply_eq_one_of_isGlobalAddChar 0 below · cited by 74 · depth 15
• Archimedean part of a global additive character is standard after twisting NumberField.AdelicFourier.exists_ne_zero_apply_eq_fourierChar_trace_of_isGlobalAddChar 6 below · cited by 15 · depth 16
• Annihilator of the integral finite adeles is d⁻¹+widehat𝒪 NumberField.AdelicFourier.forall_addChar_finitePart_mul_eq_one_iff_exists_mem_traceDual 4 below · cited by 4 · depth 17
• Dilation rule for the adelic Fourier transform NumberField.AdelicFourier.fourierIntegral_comp_mul_left 0 below · cited by 10 · depth 17
• Adelic Fourier inversion with an unnormalised Haar measure NumberField.AdelicFourier.fourierIntegral_fourierIntegral_eq 33 below · cited by 3 · depth 17
• Fourier transform preserves the adelic Schwartz–Bruhat space NumberField.AdelicFourier.fourierIntegral_mem_schwartzBruhat 19 below · cited by 11 · depth 17
• Product formula for the adelic Fourier transform of a pure tensor NumberField.AdelicFourier.fourierIntegral_pureTensor_eq 0 below · cited by 8 · depth 17
• Schwartz–Bruhat functions on A_F are Haar-integrable NumberField.AdelicFourier.integrable_of_mem_schwartzBruhat 0 below · cited by 20 · depth 17
• Self-annihilation of F in A_F under a global character NumberField.AdelicFourier.mem_range_algebraMap_of_forall_apply_mul_eq_one 1 below · cited by 4 · depth 17
• Adelic Poisson summation with the zero frequency split off NumberField.AdelicFourier.tsum_sub_inv_measure_mul_integral_eq_inv_measure_mul_tsum_fourierIntegral_ne_zero 37 below · cited by 9 · depth 17
• Pure tensors are stable under dilation by nonzero elements of F NumberField.AdelicFourier.comp_mul_algebraMap_mem_pureTensorSet 0 below · cited by 1 · depth 18
• Idelic dilation preserves the adelic Schwartz–Bruhat space NumberField.AdelicFourier.comp_mul_mem_schwartzBruhat 0 below · cited by 7 · depth 18
• Schwartz–Bruhat function standard outside S with non-negative Fourier multiplier NumberField.AdelicFourier.exists_mem_schwartzBruhat_isFactorizableStandardOutside_integral_eq_nonneg 52 below · cited by 1 · depth 18
• Annihilator of the integral finite adeles is the inverse different NumberField.AdelicFourier.forall_addChar_finitePart_mul_eq_one_iff_mem_traceDual 3 below · cited by 5 · depth 18
• Adelic Fourier inversion for pure tensors NumberField.AdelicFourier.fourierIntegral_fourierIntegral_eq_of_mem_pureTensorSet 28 below · cited by 2 · depth 18
• Adelic Fourier transform preserves the Schwartz–Bruhat space NumberField.AdelicFourier.fourierIntegral_mem_schwartzBruhat_of_apply_eq_fourierChar_trace 13 below · cited by 6 · depth 18
• Factorisation of the finite-adelic Fourier transform of an S-standard function NumberField.AdelicFourier.inv_measure_mul_fourierIntegral_finiteAdeleRing_prod_mul_indicator_eq 1 below · cited by 2 · depth 18
• Standard functions on the finite adeles are locally constant with compact support NumberField.AdelicFourier.isLocallyConstant_and_hasCompactSupport_prod_mul_ite_forall_mem_adicCompletionIntegers 0 below · cited by 6 · depth 18
• Summability of Schwartz–Bruhat translates over the principal adeles NumberField.AdelicFourier.summable_translate_of_mem_schwartzBruhat 0 below · cited by 3 · depth 18
• Adelic Poisson summation on the Schwartz–Bruhat space NumberField.AdelicFourier.tsum_eq_inv_measure_mul_tsum_fourierIntegral 36 below · cited by 2 · depth 18
• Finite part of a trace-normalised global additive character at principal points NumberField.AdelicFourier.addChar_zero_finitePart_algebraMap_eq_fourierChar_neg_trace 1 below · cited by 3 · depth 19
• Uniform polynomial height moments of Schwartz–Bruhat functions NumberField.AdelicFourier.exists_forall_integral_norm_mul_inv_adelicHeight_mul_unipotentGL2_pow_le_of_mem_schwartzBruhat 3 below · cited by 1 · depth 19
• Product bump functions on the infinite adeles NumberField.AdelicFourier.exists_schwartzMap_comp_ringEquiv_mixedSpace_eq_prod 0 below · cited by 1 · depth 19
• Adelic Fourier inversion for pure tensors NumberField.AdelicFourier.fourierIntegral_fourierIntegral_eq_of_mem_pureTensorSet_of_apply_eq_fourierChar_trace 19 below · cited by 1 · depth 19
• Fourier transform of the dual lattice of mathcal Oᵥ NumberField.AdelicFourier.fourierIntegral_indicator_setOf_forall_mem_adicCompletionIntegers_apply_mul_eq_one 0 below · cited by 1 · depth 19
• Factorisation of the archimedean Fourier integral over infinite places NumberField.AdelicFourier.integral_fourierChar_trace_mul_prod_eq_prod_integral_fourierChar_trace_single_mul 0 below · cited by 1 · depth 19
• Finite-adelic Fourier transform preserves Schwartz–Bruhat functions NumberField.AdelicFourier.isLocallyConstant_and_hasCompactSupport_fourierIntegral_finiteAdeleRing 7 below · cited by 3 · depth 19
• Pushforward of per-place Lebesgue measures is mixed-space volume NumberField.AdelicFourier.map_ringEquiv_mixedSpace_pi_eq_volume 0 below · cited by 1 · depth 19
• Level-zero additive character: the dual of mathcal Oᵥ is mathcal Oᵥ NumberField.AdelicFourier.setOf_forall_mem_adicCompletionIntegers_apply_mul_eq_one_eq_of_level_zero 0 below · cited by 1 · depth 19
• Adelic Poisson summation with translation NumberField.AdelicFourier.tsum_translate_eq_inv_measure_mul_tsum_fourierIntegral 35 below · cited by 1 · depth 19
• Pure tensors on the adele ring are translation-stable NumberField.AdelicFourier.comp_add_right_mem_pureTensorSet 0 below · cited by 1 · depth 20
• Uniqueness of additive Haar measure on A_F NumberField.AdelicFourier.exists_smul_eq_of_isAddHaarMeasure_adeleRing 0 below · cited by 4 · depth 20
• Fourier inversion on the finite adeles with explicit constant NumberField.AdelicFourier.fourierIntegral_fourierIntegral_finiteAdeleRing_eq 12 below · cited by 1 · depth 20
• Integrability of a decaying archimedean times locally constant finite factor NumberField.AdelicFourier.integrable_mul_of_continuous_of_decay_of_isLocallyConstant 0 below · cited by 2 · depth 20
• Compactness and openness of the annihilator of widehat𝒪_F NumberField.AdelicFourier.isCompact_and_isOpen_setOf_forall_addChar_finitePart_mul_eq_one 5 below · cited by 4 · depth 20
• Adelic Poisson summation for pure tensors, unnormalised measure NumberField.AdelicFourier.tsum_eq_inv_measure_mul_tsum_fourierIntegral_of_mem_pureTensorSet 25 below · cited by 1 · depth 20
• Integrable domination of archimedean translates of a Schwartz–Bruhat function NumberField.AdelicFourier.exists_integrable_forall_norm_comp_sub_smul_le 0 below · cited by 1 · depth 21
• Archimedean directional derivatives of Schwartz–Bruhat functions on A_F NumberField.AdelicFourier.exists_mem_schwartzBruhat_hasDerivAt_comp_sub_smul 0 below · cited by 1 · depth 21
• Double annihilator of the integral finite adeles NumberField.AdelicFourier.forall_addChar_finitePart_mul_eq_one_of_forall_iff_mem_integralFiniteAdeles 4 below · cited by 1 · depth 21
• Finite-adelic Fourier transform of a principal coset indicator NumberField.AdelicFourier.fourierIntegral_indicator_principalCoset_finiteAdeleRing_apply 0 below · cited by 1 · depth 21
• Haar volume of the annihilator of widehat𝒪_F NumberField.AdelicFourier.measure_setOf_forall_addChar_finitePart_mul_eq_one 6 below · cited by 1 · depth 21
• Character orthogonality over a compact subgroup of the finite adeles NumberField.AdelicFourier.setIntegral_addChar_mul_eq_ite_of_isCompact 0 below · cited by 1 · depth 21
• Adelic Poisson summation for pure tensors, normalised Haar measure NumberField.AdelicFourier.tsum_eq_tsum_fourierIntegral_of_mem_pureTensorSet_of_measure_adelicBox_eq_one 24 below · cited by 1 · depth 21
• Adelic Poisson summation for pure tensors, normalised NumberField.AdelicFourier.tsum_eq_tsum_fourierIntegral_of_mem_pureTensorSet_of_apply_eq_fourierChar_trace 20 below · cited by 1 · depth 22
• Finite-adelic Fourier transform of a principal-coset indicator NumberField.AdelicFourier.fourierIntegral_indicator_principalCoset_finiteAdeleRing 0 below · cited by 2 · depth 23
• Summability of a pure adelic tensor over principal points NumberField.AdelicFourier.summable_comp_algebraMap_of_mem_pureTensorSet 2 below · cited by 1 · depth 23
• Basic properties of two-variable adelic Schwartz–Bruhat functions NumberField.AdelicFourier.continuous_integrable_comp_vecMul_mem_and_bottomRowVec_mem_schwartzBruhat_of_mem_schwartzBruhat2 1 below · cited by 15 · depth 25
• Godement's bound for the truncated theta integral on a Siegel set NumberField.AdelicFourier.exists_forall_setIntegral_tsum_norm_apply_smul_vecMul_mul_rpow_le_mul_archHeight_pow_of_mem_integralWindowedSiegelSet 65 below · cited by 5 · depth 25
• Convergence and decay of adelic theta series on GL₂ NumberField.AdelicFourier.exists_forall_tsum_norm_apply_smul_vecMul_le_and_continuous_tsum_of_mem_schwartzBruhat2 5 below · cited by 7 · depth 25
• Gaussian times indicator as a Schwartz–Bruhat function on A_ℚ² NumberField.AdelicFourier.exists_mem_schwartzBruhat2_apply_bottomRowVec_eq_gaussian_mul_indicator_rat 1 below · cited by 1 · depth 25
• Schwartz–Bruhat space of pairs is stable under adelic Fourier transform NumberField.AdelicFourier.fourierTransform2_mem_schwartzBruhat2_and_reflectPair_mem_schwartzBruhat2 26 below · cited by 8 · depth 25
• Adelic theta transformation formula on GL₂ NumberField.AdelicFourier.tsum_apply_smul_vecMul_add_eq_ideleNorm_cpow_neg_two_mul_tsum_reflectPair_of_mem_schwartzBruhat2 26 below · cited by 6 · depth 25
• Module of GL₂(A_F) acting on adelic row vectors NumberField.AdelicFourier.addHaar_image_vecMul_eq_ideleNorm_det_mul_and_fourierTransform2_comp_vecMul 1 below · cited by 3 · depth 26
• Uniform convergence and decay of an adelic theta series NumberField.AdelicFourier.exists_forall_tsum_norm_apply_vecMul_le_of_mem_schwartzBruhat2_of_isCompact 3 below · cited by 1 · depth 26
• Adelic Poisson summation in two variables NumberField.AdelicFourier.tsum_eq_inv_measure_sq_mul_tsum_fourierTransform2_of_mem_schwartzBruhat2 23 below · cited by 2 · depth 26
• Godement's estimate on GL₂(A_ℚ), small-norm half NumberField.AdelicFourier.exists_forall_setIntegral_norm_le_one_tsum_norm_apply_smul_vecMul_mul_rpow_le_mul_archHeight_pow_of_mem_integralWindowedSiegelSet_rat 65 below · cited by 1 · depth 27
• Schwartz–Bruhat stability of the ψ_ℚ-Fourier transform NumberField.AdelicFourier.fourierIntegral_mem_schwartzBruhat_psiQ 20 below · cited by 1 · depth 27
• Adelic Poisson summation for Schwartz times box indicator NumberField.AdelicFourier.tsum_eq_inv_measure_sq_mul_tsum_fourierTransform2_schwartzMap_mul_indicator_pi 20 below · cited by 1 · depth 27
• Theta majorant on A_ℚ² under idelic dilations NumberField.AdelicFourier.exists_forall_tsum_norm_apply_vecMul_le_mul_one_add_inv_ideleNorm_of_mem_schwartzBruhat2_rat 3 below · cited by 1 · depth 28
• Integrability of the periodisation of a pure tensor on A_F NumberField.AdelicFourier.integrableOn_tsum_translate_adelicBox_of_mem_pureTensorSet 1 below · cited by 2 · depth 29
• Fourier transform of an indicator of y+uwidehat𝒪 NumberField.AdelicFourier.fourierIntegral_indicator_coset_finiteAdeleRing_apply 0 below · cited by 2 · depth 30
• Non-negative Schwartz–Bruhat majorant for the reflected Fourier transform NumberField.AdelicFourier.exists_nonneg_mem_schwartzBruhat2_norm_reflectPair_le_and_setLIntegral_enorm_reflectPair_comp_le_lintegral_mul_ofReal_rpow 28 below · cited by 1 · depth 31
• Standard test functions on A_L²: Schwartz–Bruhat, positive finite integral NumberField.AdelicFourier.schwartzMap_mul_indicator_mem_schwartzBruhat2_and_lintegral_pairHaar_ne_zero_and_ne_top 4 below · cited by 1 · depth 31
• Domination of a Schwartz–Bruhat function and its compact translates NumberField.AdelicFourier.exists_nonneg_mem_schwartzBruhat2_forall_norm_apply_vecMul_le_of_isCompact 0 below · cited by 1 · depth 32
• Standard majorant for Schwartz–Bruhat functions on A_F² NumberField.AdelicFourier.exists_norm_le_mul_inv_one_add_norm_sq_pow_mul_indicator_integralFiniteAdeles_of_mem_schwartzBruhat2 2 below · cited by 1 · depth 32

NumberField.AdelicHaar 11

• Unimodularity of GL₂ over the adeles of a number field NumberField.AdelicHaar.isMulRightInvariant_adelicGLHaar 0 below · cited by 91 · depth 17
• Principal adeles preserve the adelic Haar measure NumberField.AdelicHaar.measurePreserving_mul_algebraMap_adelicAddHaar 2 below · cited by 20 · depth 18
• Splitting of adelic GL₂ integrals of pure tensors NumberField.AdelicHaar.exists_integral_glArch_mul_glFin_eq_mul_integral_mul_integral 2 below · cited by 6 · depth 19
• Haar measure on GL₂(A_K) in Iwasawa coordinates NumberField.AdelicHaar.exists_lintegral_adelicGLHaar_eq_mul_lintegral_iwasawa 8 below · cited by 16 · depth 19
• Adelic Haar measure on GLₙ splits as archimedean times finite NumberField.AdelicHaar.exists_map_adelicGLHaar_eq_smul_prod 1 below · cited by 5 · depth 20
• Right invariance of Haar measure on GL₂ of the archimedean adeles NumberField.AdelicHaar.isMulRightInvariant_of_isHaarMeasure_generalLinearGroup_infiniteAdeleRing 4 below · cited by 5 · depth 20
• Unimodularity of GL₃ over the adeles of ℚ NumberField.AdelicHaar.isMulRightInvariant_adelicGLHaar_finThree_rat 1 below · cited by 4 · depth 23
• Slab volumes of the quotient GLₙ(K)backslash GLₙ(A_K) NumberField.AdelicHaar.exists_measure_fundamentalDomain_inter_ideleNorm_det_Icc_eq_mul_log 5 below · cited by 3 · depth 25
• Archimedean coordinate hyperplanes of the adeles are null NumberField.AdelicHaar.adelicAddHaar_setOf_fst_apply_eq_eq_zero 3 below · cited by 1 · depth 26
• Adeles vanishing at a fixed finite place form a null set NumberField.AdelicHaar.adelicAddHaar_setOf_snd_apply_eq_zero 3 below · cited by 1 · depth 26
• Inversion invariance of the adelic Haar measure on GL₃(A_ℚ) NumberField.AdelicHaar.isInvInvariant_adelicGLHaar_finThree_rat 2 below · cited by 1 · depth 26

NumberField.AdelicHeight 14

• Upper-triangular global matrices preserve the adelic height NumberField.AdelicHeight.adelicHeight_globalPoints_mul_of_apply_one_zero_eq_zero 0 below · cited by 22 · depth 16
• Bounded distortion of the adelic height by compact right translation NumberField.AdelicHeight.exists_forall_mul_adelicHeight_le_adelicHeight_mul_of_isCompact 0 below · cited by 33 · depth 16
• Adelic height scales by the idelic norm under diag(a,1) NumberField.AdelicHeight.adelicHeight_diagOne_mul 2 below · cited by 13 · depth 20
• Continuity of the adelic height on GL₂(A_F) NumberField.AdelicHeight.continuous_adelicHeight 0 below · cited by 73 · depth 20
• Left invariance of the adelic height under B(F) NumberField.AdelicHeight.adelicHeight_globalPoints_mul_of_mem_borelSubgroup 0 below · cited by 15 · depth 28
• Right K-invariance of the adelic height on GL₂ NumberField.AdelicHeight.adelicHeight_mul_of_mem_adelicMaximalCompact 0 below · cited by 19 · depth 29
• Adelic height of diag(t,1) is the idele norm NumberField.AdelicHeight.adelicHeight_diagOne 3 below · cited by 1 · depth 30
• Left unipotent and central invariance of the adelic height NumberField.AdelicHeight.adelicHeight_unipotentGL2_mul_and_centralScalar_mul 0 below · cited by 30 · depth 30
• Idele-norm shell law and the truncated hyperbolic torus weight NumberField.AdelicHeight.exists_forall_measureReal_inter_ideleNorm_mem_Icc_eq_mul_log_and_setIntegral_weight_comp_eq 14 below · cited by 5 · depth 31
• Place-wise splitting of the base-changed adelic height weight NumberField.AdelicHeight.neg_log_adelicHeight_baseChangeGL_sub_log_adelicHeight_adelicWeyl_mul_eq_archWeight_tensorArch_add_finsum_semiLocalWeight_tensorPlace 1 below · cited by 1 · depth 32
• Diagonal invariance and continuity of the adelic height weight NumberField.AdelicHeight.neg_log_adelicHeight_sub_log_adelicHeight_adelicWeyl_mul_diagonal_mul_and_continuous 0 below · cited by 5 · depth 32
• Place splitting of the adelic Weyl height weight NumberField.AdelicHeight.neg_log_adelicHeight_sub_log_adelicHeight_adelicWeyl_mul_eq_archWeight_glArch_add_finsum_weight_finComponent 0 below · cited by 2 · depth 33
• Adelic height weight of bk depends only on its unipotent coordinate NumberField.AdelicHeight.neg_log_adelicHeight_sub_log_adelicHeight_adelicWeyl_mul_eq_unipotentGL2_of_mem_adelicBorel 5 below · cited by 1 · depth 34
• Adelic heights of a unipotent and its Weyl translate NumberField.AdelicHeight.neg_log_adelicHeight_unipotentGL2_sub_log_adelicHeight_adelicWeyl_mul_unipotentGL2_eq 0 below · cited by 1 · depth 34

NumberField.AdelicLevel 17

• Strong approximation for GL₂/ℚ at level N with positivity NumberField.AdelicLevel.exists_globalPoints_mul_mem_levelOne_rat 4 below · cited by 33 · depth 11
• Strong approximation for GL₂/ℚ at finite level K₁(N) NumberField.AdelicLevel.exists_glFin_globalPoints_mul_mem_finiteLevelOne_rat 3 below · cited by 2 · depth 12
• Every finite adelic GL₂ matrix over ℚ is globally integralisable NumberField.AdelicLevel.exists_globalPoints_mul_mem_finiteIntegralGL2_rat 0 below · cited by 5 · depth 13
• Class number one of ℚ in idelic form NumberField.AdelicLevel.finiteIdeleClassNumberOne_rat 0 below · cited by 2 · depth 15
• Rational diag(p,1) and the Hecke element at v NumberField.AdelicLevel.finEmbed_globalPoints_diag_mul_heckeGenAt_inv_mem_levelOne_rat 0 below · cited by 1 · depth 19
• Explicit left-coset representatives for the Hecke double coset at p over ℚ NumberField.AdelicLevel.isHeckeCosetSystem_levelOne_rat_of_not_dvd_absNorm 0 below · cited by 1 · depth 19
• Moving a real unipotent past diag(a,1); ψ_K at 1/2 NumberField.AdelicLevel.diagOne_mul_archRealGLAt_unipotent_eq_and_stdAddChar_single_half 0 below · cited by 4 · depth 21
• Local-to-adelic transfer of Hecke coset systems away from the level NumberField.AdelicLevel.isHeckeCosetSystem_padicToAdelic_of_isHeckeCosetSystem_integralSubgroup 0 below · cited by 1 · depth 21
• Factorisation of diag(a,1) at a real place NumberField.AdelicLevel.diagOne_eq_diagOne_mul_archRealLiftAt_mul_centralScalar 0 below · cited by 3 · depth 22
• Finite-place entry bounds for an adelic alignment element NumberField.AdelicLevel.valued_apply_mul_diagOne_inv_mul_diagOne_mul_le_of_valued_eq 0 below · cited by 1 · depth 22
• Hecke generator inverse double-coset relation at level U₁(N) NumberField.AdelicLevel.exists_heckeGen_inv_eq_centralScalar_mul_mul_heckeGen_mul_levelOne 1 below · cited by 1 · depth 23
• Double-coset inversion relation for Hecke generators at principal level NumberField.AdelicLevel.exists_heckeGen_inv_eq_centralScalar_mul_mul_heckeGen_mul_principalLevel 1 below · cited by 2 · depth 23
• Inverse of the Hecke generator in its level-N double coset NumberField.AdelicLevel.exists_heckeGen_inv_eq_centralScalar_mul_mul_heckeGen_mul_levelOne_and_mul_det_eq_one 0 below · cited by 1 · depth 24
• Hecke generator inverse in a central-times-level double coset NumberField.AdelicLevel.exists_heckeGen_inv_eq_centralScalar_mul_mul_heckeGen_mul_of_forall_finEmbed_localEmbed_mem 0 below · cited by 2 · depth 24
• Central unit idele at v ∤ N lies in U(N) NumberField.AdelicLevel.centralScalar_finIncl_localUnit_mem_principalLevel_inf_finiteAdelicGL2Subgroup 0 below · cited by 2 · depth 29
• Principal congruence subgroups are a neighbourhood basis at 1 NumberField.AdelicLevel.exists_finset_forall_mem_of_valued_sub_le_of_mem_nhds_one 0 below · cited by 3 · depth 30
• Maximal compact conjugation preserves the principal level NumberField.AdelicLevel.conj_mem_principalLevel_inf_finiteAdelicGL2Subgroup_of_mem_adelicMaximalCompact 0 below · cited by 4 · depth 33

NumberField.AdelicTrace 1

• Finite-adelic trace is the sum of local traces above p NumberField.AdelicTrace.traceFinHom_apply_eq_sum_trace 0 below · cited by 1 · depth 18

NumberField.AdicCompletion 6

• Haar measure under a linear map over Kᵥ NumberField.AdicCompletion.map_linearMap_eq_norm_det_inv_smul_of_isAddHaarMeasure 2 below · cited by 17 · depth 28
• Haar measure on Kᵥ^ι scales by |det M| NumberField.AdicCompletion.map_matrix_mulVec_pi_eq_smul_pi 1 below · cited by 6 · depth 28
• Jacobian identity for the torus chart on GL₂(Kᵥ) NumberField.AdicCompletion.lintegral_comp_torusAffineChart_mul_eq_lintegral 1 below · cited by 1 · depth 33
• Multiplicative annuli in Kᵥ lie in dilates of one compact set NumberField.AdicCompletion.exists_isCompact_forall_setOf_le_norm_pow_le_subset_smul 0 below · cited by 1 · depth 36
• Finiteness of int max(1,‖y‖)⁻² dν on L_w NumberField.AdicCompletion.lintegral_inv_max_one_norm_sq_lt_top 3 below · cited by 1 · depth 36
• Jacobian of the torus–unipotent product chart over L⊗_K Kᵥ NumberField.AdicCompletion.lintegral_tensor_comp_splitTorusProductChart_mul_norm_algebraNorm_eq_lintegral 3 below · cited by 1 · depth 37

NumberField.ArchIdele 3

• Tate groups of the archimedean idèle module NumberField.ArchIdele.card_tateH0_obj_eq_prod_and_subsingleton_tateHneg1 9 below · cited by 1 · depth 20
• Archimedean idèle fibre as coinduced local units NumberField.ArchIdele.exists_addEquiv_coind_localUnits 3 below · cited by 1 · depth 20
• Coinduced archimedean units as the product over places above v NumberField.ArchIdele.exists_addEquiv_coind_localUnits_transportUnits_apply 3 below · cited by 2 · depth 20

NumberField.FinitePlace 2

• Uniform bound for |log ν(z)| in terms of -log ν(p) NumberField.FinitePlace.exists_abs_log_le_mul_neg_log_of_coe_eq 0 below · cited by 1 · depth 18
• Finite places extend, up to a positive real power NumberField.FinitePlace.exists_finitePlace_inclusion_eq_rpow 0 below · cited by 1 · depth 18

NumberField.FiniteSIdele 6

• Tate groups of the finite S-idèle module NumberField.FiniteSIdele.card_tateH0_obj_eq_prod_and_subsingleton_tateHneg1 24 below · cited by 1 · depth 20
• Coinduced local integral units as the product over places above v NumberField.FiniteSIdele.exists_addEquiv_coind_localIntegerUnits 6 below · cited by 2 · depth 20
• Coinduced local integral units as the product over w ∣ v NumberField.FiniteSIdele.exists_addEquiv_coind_localIntegerUnits_transportIntegerUnits_apply 6 below · cited by 2 · depth 20
• Coinduced local unit module is the product over places above v NumberField.FiniteSIdele.exists_addEquiv_coind_localUnits 6 below · cited by 1 · depth 20
• Coinduced local units at v as the product over w ∣ v NumberField.FiniteSIdele.exists_addEquiv_coind_localUnits_transportUnits_apply 6 below · cited by 2 · depth 20
• Vanishing of Hⁿ⁺¹ for unramified local integral units NumberField.FiniteSIdele.isZero_groupCohomology_pi_coind_localIntegerUnits_of_ramificationIdx_eq_one 16 below · cited by 1 · depth 22

NumberField.Idele 37

• Positive finite volume of norm slabs in a fundamental domain NumberField.Idele.idelicHaar_inter_setOf_ideleNorm_mem_Icc_pos_and_lt_top 15 below · cited by 14 · depth 16
• Archimedean idelic measure as Lebesgue measure with Haar density NumberField.Idele.exists_map_ringEquiv_mixedSpace_sPartMeasure_empty_eq_smul_withDensity 0 below · cited by 3 · depth 18
• Polar coordinates for the empty-part idelic Haar measure NumberField.Idele.exists_lintegral_prod_norm_sPartMeasure_empty_eq_mul_prod_lintegral 0 below · cited by 6 · depth 20
• Norm slabs in a fundamental domain have r-independent idelic volume NumberField.Idele.exists_setLIntegral_indicator_ideleNorm_sq_mul_mem_Icc_eq_const 16 below · cited by 13 · depth 20
• Factoring an idelic integral over the places outside S NumberField.Idele.lintegral_mul_finprod_eq_lintegral_sPartMeasure_mul_iSup 0 below · cited by 1 · depth 20
• Splitting of the S-part idelic measure over ℤ^S NumberField.Idele.lintegral_mul_prod_ord_sPartMeasure_eq_lintegral_sPartMeasure_empty_mul_prod_tsum 0 below · cited by 4 · depth 21
• Positivity of the S-part measure at an idele trivial outside S NumberField.Idele.sPartMeasure_pos_of_isOpen_of_partAt_eq 0 below · cited by 1 · depth 21
• Splitting of integrals for the S-part of idelic Haar measure NumberField.Idele.exists_integral_sPartMeasure_eq_mul_integral_mul_prod_integral 0 below · cited by 2 · depth 22
• Norm disintegration of idelic Haar measure on a fundamental domain NumberField.Idele.exists_setLIntegral_comp_ideleNorm_eq_mul_lintegral_Ioi 17 below · cited by 12 · depth 22
• Integrability criterion for the S-part measure via a product majorant NumberField.Idele.integrable_sPartMeasure_of_norm_le_mul_prod 0 below · cited by 1 · depth 22
• Right translation invariance of the S-part idelic measure NumberField.Idele.measurePreserving_mul_right_sPartMeasure 0 below · cited by 3 · depth 22
• An archimedean twist makes a non-trivial idele integral non-zero NumberField.Idele.exists_integral_stdAddChar_mul_ne_zero_of_continuous_of_integrable_sPartMeasure_empty 9 below · cited by 2 · depth 23
• Two-sided archimedean decay implies integrability for ν_∅ NumberField.Idele.integrable_sPartMeasure_empty_of_norm_le_ideleNorm_rpow_mul_prod_min_one_rpow_of_norm_le_rpow_neg 6 below · cited by 5 · depth 23
• A ball indicator at S integrates out of the S-part measure NumberField.Idele.exists_lintegral_ite_ball_comp_partAt_sPartMeasure_eq_mul_lintegral_sPartMeasure_empty 2 below · cited by 1 · depth 24
• Uniqueness of Haar measure on the idele group NumberField.Idele.exists_forall_measure_eq_mul_idelicHaar 0 below · cited by 1 · depth 30
• Existence of a product-measure datum with prescribed ord and S-part NumberField.Idele.exists_productMeasureData_ord_eq_and_projS_eq_and_smul_eq_map_partAt 0 below · cited by 2 · depth 30
• Shift-invariance and finiteness of idelic norm shells NumberField.Idele.idelicHaar_inter_setOf_mul_ideleNorm_sq_mem_Icc_eq 16 below · cited by 1 · depth 30
• Semi-local coordinates on A_L^×: topology, surjectivity, compact boxes NumberField.Idele.secondCountableTopology_and_semiLocalUnits_and_archUnits_and_integralUnits_and_surjective_and_isCompact_box 23 below · cited by 12 · depth 30
• Local norm of a principal idele as a power of ‖varpiᵥ‖ NumberField.Idele.norm_algebraMap_adicCompletion_eq_norm_uniformizer_zpow_ord 0 below · cited by 2 · depth 31
• Unramified idele character: S-part times uniformiser powers at T NumberField.Idele.apply_eq_apply_partAt_mul_prod_apply_det_heckeGen_zpow_ord_of_mem_unitIdelesOutside 1 below · cited by 4 · depth 32
• The ξ-fold of local windows is a global window NumberField.Idele.contDiff_and_exists_isCompact_and_isLocallyConstant_integral_mul_window_prod_map_partAt_of_isCompact 2 below · cited by 5 · depth 32
• Splicing an idele from prescribed local components NumberField.Idele.exists_fst_eq_and_snd_eq_of_mem_and_snd_eq_of_mem_and_snd_eq_one 0 below · cited by 1 · depth 32
• Unfolding a translated idele integral off S∪ T NumberField.Idele.integral_mul_indicator_unitIdelesOutside_mul_prod_translate_eq_mul_integral_mul_prod_tsum 2 below · cited by 2 · depth 32
• Semi-local factorisation of a continuous idelic character NumberField.Idele.exists_finset_forall_semiLocalCharacter_eq_one_and_eq_mul_prod_semiLocalCharacter_of_continuous 0 below · cited by 1 · depth 33
• Factorisation of Haar measure on the ideles of L over places of K NumberField.Idele.exists_forall_lintegral_and_integral_eq_mul_prod_semiLocalIdele_of_isHaarMeasure 28 below · cited by 1 · depth 33
• Tilt modulus along T-units as an exponential linear form NumberField.Idele.exists_linearMap_exp_apply_eq_prod_norm_sqrt_mul_zpow_neg_of_apply_det_heckeGen_pow_eq 16 below · cited by 2 · depth 33
• Centre unfolding of an Euler-bracket idele integrand NumberField.Idele.integral_mul_prod_mul_finprod_mul_apply_translate_eq_mul_ideleNorm_partAt_mul_prod_tsum_mul_integral 9 below · cited by 1 · depth 33
• Continuity of semi-local idele components, finite and archimedean NumberField.Idele.continuous_semiLocalIdele_and_continuous_archSemiLocalIdele 23 below · cited by 2 · depth 34
• Haar measure on A_L^× factorises over places of K NumberField.Idele.exists_forall_lintegral_eq_mul_lintegral_mul_prod_lintegral_semiLocalIdele_of_isHaarMeasure 27 below · cited by 1 · depth 34
• Splitting of the idelic ξ-fold of a kinked archimedean window NumberField.Idele.integral_mul_kinkWindow_prod_map_partAt_eq_add_sum_real_add_sum_complex_of_isCompact 3 below · cited by 3 · depth 34
• Compactness of semi-local idele boxes in A_L^× NumberField.Idele.isCompact_setOf_archSemiLocalIdele_mem_and_semiLocalIdele_mem 0 below · cited by 1 · depth 34
• Folded archimedean discrepancy window over the S-part idele measure NumberField.Idele.exists_contDiff_integral_mul_discArchWindow_prod_eq_add_sum_norm_sub_inv_mul_add_sum_of_isCompact 6 below · cited by 1 · depth 35
• Smoothness of ξ-twisted adelic window integrals in the archimedean parameter NumberField.Idele.integrable_and_contDiff_integral_mul_comp_ringEquiv_mixedSpace_mul_prod_map_partAt 2 below · cited by 3 · depth 35
• Continuous functions on A_F^×timesK are a.e. strongly measurable NumberField.Idele.aestronglyMeasurable_of_continuous_prod_maximalCompact 1 below · cited by 3 · depth 38
• Invariance of the weighted idele × K integral NumberField.Idele.lintegral_comp_mul_norm_one_mul_maximalCompact_eq_of_isFundamentalDomain_of_periodic 4 below · cited by 1 · depth 38
• Finite mass of a norm band for ‖t‖⁻¹d^× t⊗ dk NumberField.Idele.withDensity_inv_ideleNorm_restrict_prod_maximalCompactHaar_band_lt_top 16 below · cited by 1 · depth 38
• Haar measure on the idele class group via a fundamental domain NumberField.Idele.t2Space_and_secondCountable_and_locallyCompact_and_exists_isHaarMeasure_map_mk_restrict_of_isFundamentalDomain 3 below · cited by 1 · depth 39

NumberField.IdeleClassGroup 10

• Second inequality: #H²(S,C_F)≤ |S| for all subgroups NumberField.IdeleClassGroup.finite_H2_and_natCard_H2_le_card 131 below · cited by 2 · depth 21
• Vanishing of H¹ of the idèle class group NumberField.IdeleClassGroup.isZero_H1 126 below · cited by 2 · depth 21
• Invariant idèle classes are norms from the compositum NumberField.IdeleClassGroup.exists_sum_rho_pow_eq_of_forall_rho_eq 149 below · cited by 2 · depth 22
• Finiteness and order bound for H²(S,C_F) in a p-extension NumberField.IdeleClassGroup.finite_H2_and_natCard_H2_le_card_of_isPGroup 124 below · cited by 4 · depth 22
• Vanishing of H¹ of idele classes over a p-extension NumberField.IdeleClassGroup.isZero_H1_of_isPGroup 119 below · cited by 7 · depth 22
• Galois descent for idele classes at an intermediate field NumberField.IdeleClassGroup.nonempty_quotientToInvariants_iso_of_isScalarTower 1 below · cited by 2 · depth 22
• Restriction to S agrees with descent to the fixed field NumberField.IdeleClassGroup.nonempty_res_iso_fixedField_and_groupCohomology_iso 2 below · cited by 6 · depth 22
• H¹ vanishes and #H² = #S for idele classes at prime-order S NumberField.IdeleClassGroup.isZero_H1_and_natCard_H2_eq_card_of_card_prime 117 below · cited by 3 · depth 23
• H¹ vanishes and #H² = #S at every cyclic subgroup NumberField.IdeleClassGroup.isZero_H1_and_natCard_H2_eq_card_of_isCyclic 119 below · cited by 1 · depth 23
• Galois descent for idele classes: C_F^N ≅ C_{F^N} NumberField.IdeleClassGroup.nonempty_quotientToInvariants_iso_fixedField 1 below · cited by 3 · depth 23

NumberField.IdeleLocalInv 11

• Uniqueness of the local invariant at a finite place NumberField.IdeleLocalInv.eq_of_hasLocalInv 112 below · cited by 3 · depth 24
• Existence of a local invariant at each finite place of E NumberField.IdeleLocalInv.exists_hasLocalInv 99 below · cited by 3 · depth 24
• Transport data along an automorphism of a Galois layer NumberField.IdeleLocalInv.exists_transport_data_of_algEquiv 5 below · cited by 1 · depth 24
• Local invariant depends only on the finite coordinates NumberField.IdeleLocalInv.hasLocalInv_iff_of_forall_map_prG_eq 0 below · cited by 1 · depth 24
• Transport of a local invariant along an isomorphism of Galois layers NumberField.IdeleLocalInv.hasLocalInv_map_of_ringEquiv 6 below · cited by 1 · depth 24
• Capitulation realises p-primary idèle classes by S-unit cocycles NumberField.IdeleLocalInv.exists_cocyclesTwo_sUnitsRep_hasLocalInv_of_map_pi_eq_zero_of_capitulation 157 below · cited by 1 · depth 25
• Prescribed sum-zero local invariants on degree-two idèle cohomology NumberField.IdeleLocalInv.exists_pow_smul_eq_zero_and_map_pi_eq_zero_and_hasLocalInv 378 below · cited by 1 · depth 25
• S-unit realisation of p-primary H² classes after capitulation NumberField.IdeleLocalInv.exists_cocyclesTwo_sUnitsRep_map_toUnitsRep_eq_of_capitulation 44 below · cited by 1 · depth 26
• p-primary lift of an idèle class to H²(G,K^×) NumberField.IdeleLocalInv.exists_zsmul_eq_zero_and_map_eq_of_map_pi_eq_zero 4 below · cited by 1 · depth 26
• Local invariants survive genuine adèlic base change NumberField.IdeleLocalInv.hasLocalInv_map_genuineBaseChange 119 below · cited by 1 · depth 26
• Capitulation kills p-primary classes dying in the idèles NumberField.IdeleLocalInv.map_eq_zero_of_zsmul_eq_zero_of_map_eq_zero_of_capitulation 12 below · cited by 1 · depth 27

NumberField.InfPlaceDecomp 12

• Archimedean local bridge in degree one at a complex place NumberField.InfPlaceDecomp.exists_isLocalBridge1_archimedean 5 below · cited by 2 · depth 19
• Injective archimedean local bridge at an infinite place NumberField.InfPlaceDecomp.exists_isLocalBridge2_archimedean 4 below · cited by 1 · depth 19
• Complex conjugation generates decomposition groups at infinite places NumberField.InfPlaceDecomp.exists_restrictNormalHom_conj_complexConjugation_mem_decomp 0 below · cited by 2 · depth 19
• Archimedean local-bridge hypotheses: level, divisibility, degree-one acyclicity NumberField.InfPlaceDecomp.localBridge_hypotheses_archimedean 1 below · cited by 3 · depth 19
• Orbit–stabiliser for infinite places in a Galois extension NumberField.InfPlaceDecomp.card_over_mul_card_decomp_above 0 below · cited by 1 · depth 20
• Infinite places of a Galois extension as a G-set NumberField.InfPlaceDecomp.exists_equiv_sigma_quotient_decomp_above 0 below · cited by 1 · depth 20
• Infinite places of K^H count H-orbits on coprodᵥ G/Dᵥ NumberField.InfPlaceDecomp.card_infinitePlace_fixedField_eq_card_orbitRel_quotient 0 below · cited by 1 · depth 21
• Tate cohomology of the units at an infinite place NumberField.InfPlaceDecomp.card_tateH0_units_eq_card_and_subsingleton_tateHneg1 2 below · cited by 1 · depth 21
• Trivial decomposition at infinity over a Sylow fixed field NumberField.InfPlaceDecomp.eq_one_of_mem_decomp_fixedField_sylow 0 below · cited by 1 · depth 22
• Nontrivial elements of D_w act as complex conjugation NumberField.InfPlaceDecomp.extensionEmbedding_smul_of_ne_one 0 below · cited by 1 · depth 22
• Infinite places of C^M have trivial decomposition group NumberField.InfPlaceDecomp.eq_one_of_mem_decomp_fixedField_of_forall_isConj_mem 0 below · cited by 1 · depth 23
• Trivial archimedean decomposition groups when √-1∈ E NumberField.InfPlaceDecomp.eq_one_of_mem_decomp_of_sq_eq_neg_one 0 below · cited by 2 · depth 24

NumberField.InfiniteAdeleRing 15

• The infinite adele ring is homeomorphic to the mixed space NumberField.InfiniteAdeleRing.isHomeomorph_ringEquiv_mixedSpace 0 below · cited by 21 · depth 22
• Nondegeneracy of the real trace forms on K_∞ and L⊗_K K_∞ NumberField.InfiniteAdeleRing.traceForm_nondegenerate_and_traceForm_tensorProduct_nondegenerate 0 below · cited by 1 · depth 29
• Factorisable polynomial-times-Gaussian archimedean functions are Schwartz NumberField.InfiniteAdeleRing.exists_schwartzMap_apply_ringEquiv_mixedSpace_eq_prod_of_polynomial_mul_gaussian 0 below · cited by 1 · depth 30
• Haar measure on GLₙ of the infinite adeles via |N|⁻¹ dX NumberField.InfiniteAdeleRing.exists_isHaarMeasure_lintegral_eq_setLIntegral_inv_abs_norm_mixedSpace 0 below · cited by 1 · depth 31
• Modulus of a continuous character of K_∞^× NumberField.InfiniteAdeleRing.exists_norm_apply_units_eq_prod_norm_rpow_of_continuous 0 below · cited by 2 · depth 32
• Regrouping the infinite adelic unit group over places of K NumberField.InfiniteAdeleRing.exists_continuousMulEquiv_units_pi_forall_apply_eq_archFibre 0 below · cited by 4 · depth 33
• Archimedean Iwasawa decomposition and compactness of K_∞ NumberField.InfiniteAdeleRing.exists_mem_borelSubgroup_mul_eq_and_isCompact_iInf_rowIsometrySubgroup 4 below · cited by 19 · depth 33
• Archimedean norms split over the infinite places NumberField.InfiniteAdeleRing.mem_range_norm_tensorProduct_iff_forall_infinitePlace 0 below · cited by 3 · depth 33
• Modulus of a unit acting on the infinite adele ring NumberField.InfiniteAdeleRing.distribHaarChar_eq_prod_norm_pow_mult 0 below · cited by 3 · depth 34
• Iwasawa integration formula for GL₂(K_∞) NumberField.InfiniteAdeleRing.exists_lintegral_generalLinearGroup_eq_mul_lintegral_scalar_diagUnits2_unipotentGL2_rowIsometry 12 below · cited by 3 · depth 34
• Norms on K_∞ via the infinite places of K NumberField.InfiniteAdeleRing.norm_algebraMap_apply_eq_and_prod_pow_mult_eq_norm 0 below · cited by 1 · depth 34
• Archimedean Borel Haar measure in z(u)a(t)n(x) coordinates NumberField.InfiniteAdeleRing.exists_lintegral_borelSubgroup_eq_mul_lintegral_scalar_diagUnits2_unipotentGL2 0 below · cited by 1 · depth 35
• Haar measure of norm shells in K_∞^× NumberField.InfiniteAdeleRing.measure_setOf_forall_le_norm_apply_le_mul_eq_and_pos_and_lt_top 0 below · cited by 1 · depth 35
• The unit group of K_∞ carries the subspace topology NumberField.InfiniteAdeleRing.isEmbedding_units_val 0 below · cited by 7 · depth 36
• Module of a K_∞-linear automorphism of a finite free module NumberField.InfiniteAdeleRing.map_linearMap_eq_inv_prod_norm_archEval_det_pow_mult_smul_of_isAddHaarMeasure 1 below · cited by 2 · depth 37

NumberField.InfinitePlace 10

• Sign of the norm as product of signs at real places NumberField.InfinitePlace.sign_norm_eq_prod_sign_embedding_of_isReal 0 below · cited by 2 · depth 16
• Uniform decay of lattice sums over s⁻¹𝒪_F NumberField.InfinitePlace.exists_sum_prod_inv_one_add_mul_pow_le 1 below · cited by 2 · depth 17
• Signature of a cubic field: three real places, or one real and one complex NumberField.InfinitePlace.exists_isReal_and_three_real_or_one_complex_of_finrank_eq_three 0 below · cited by 1 · depth 19
• Infinite places unramified in Kummer extensions E(u^{1/p}) NumberField.InfinitePlace.isUnramifiedIn_of_pow_eq 0 below · cited by 1 · depth 19
• Every element of a complex completion is an n-th power NumberField.InfinitePlace.natCard_units_completion_quotient_range_powMonoidHom_of_isComplex 0 below · cited by 1 · depth 19
• Real place: index of n-th powers in K_w^× NumberField.InfinitePlace.natCard_units_completion_quotient_range_powMonoidHom_of_isReal 0 below · cited by 1 · depth 19
• Unit groups of complex completions are divisible NumberField.InfinitePlace.exists_pow_eq_of_isTotallyComplex 0 below · cited by 1 · depth 20
• Openness of n-th powers in K_w^× at an infinite place NumberField.InfinitePlace.isOpen_range_powMonoidHom_units_completion 0 below · cited by 1 · depth 26
• Unramified infinite place gives a K-embedding of L into Kᵥ NumberField.InfinitePlace.nonempty_algHom_completion_of_isUnramified 0 below · cited by 4 · depth 30
• Continuous quasi-characters of F_w^× as powers on positive reals NumberField.InfinitePlace.Completion.exists_forall_apply_eq_cpow_of_extensionEmbedding_eq_of_continuous 1 below · cited by 1 · depth 33

NumberField.InfinitePlaceTransport 4

• Transport along the identity automorphism is the identity NumberField.InfinitePlaceTransport.transport_one 0 below · cited by 4 · depth 18
• Transport of completions is compatible with composition NumberField.InfinitePlaceTransport.transport_trans_transport 0 below · cited by 6 · depth 18
• Transport of archimedean completions commutes with base change NumberField.InfinitePlaceTransport.transport_algebraMap_completion 0 below · cited by 1 · depth 19
• Transport along σ equals the decomposition-group action on K_w NumberField.InfinitePlaceTransport.transport_eq_actRingEquiv 0 below · cited by 5 · depth 21

NumberField.LevelArith 85

• Equivariant mod-p S-unit rank formula with coefficients NumberField.LevelArith.finrank_invariants_unitsModP_tensor_add_finrank_invariants_eq 48 below · cited by 1 · depth 19
• Normality of the level field under conjugation-stability NumberField.LevelArith.normal_levelField_of_isNormalLevel 0 below · cited by 7 · depth 19
• Archimedean places of a level as Γ_L-orbits NumberField.LevelArith.exists_placesAbove_inl_equiv_infinitePlace 0 below · cited by 1 · depth 20
• Places of the level above q as primes of 𝒪_{L'} NumberField.LevelArith.exists_placesAbove_inr_embedding_heightOneSpectrum 11 below · cited by 2 · depth 20
• Invariant S-level classes have the dimension of Selmer tensor invariants NumberField.LevelArith.finiteDimensional_and_finrank_continuousH1Sr_res_inf_eq_finrank_invariants_selmerRep_tensor 23 below · cited by 1 · depth 20
• Additivity of twisted invariants in the S-Selmer sequence NumberField.LevelArith.finrank_invariants_selmerRep_tensor_eq_unitsModP_add_sClassTorsionP 7 below · cited by 1 · depth 20
• Order of Gal(L/K) as a relative index NumberField.LevelArith.natCard_levelGal_eq_relIndex 0 below · cited by 1 · depth 20
• p-torsion of the S-units is 𝔽ₚ(χ) NumberField.LevelArith.nonempty_inflLevel_repTorsionP_sUnitsRep_iso_twist_cycloChar 0 below · cited by 1 · depth 20
• Embedding of H¹_S into the S-class group NumberField.LevelArith.exists_continuousH1Sr_sUnitsMaxRep_linearMap_sClassGroupRep_injective 17 below · cited by 1 · depth 21
• Equivariant embedding of H¹_S into the S-class group NumberField.LevelArith.exists_continuousH1Sr_sUnitsMaxRep_linearMap_sClassGroupRep_injective_natural 17 below · cited by 1 · depth 21
• Capitulation of p-power-torsion ideal classes in a Galois S-level NumberField.LevelArith.exists_le_isUnramifiedOutside_isGalois_forall_map_isPrincipal 8 below · cited by 2 · depth 21
• Primes above q as Γ_L-orbits on Γ/D_q NumberField.LevelArith.exists_placesAbove_inr_equiv_primesOver 12 below · cited by 2 · depth 21
• Transporting p-torsion of the S-class group to the level representation NumberField.LevelArith.exists_restrict_and_torsionBy_sClassGroupRep_linearEquiv_sClassTorsionP 1 below · cited by 1 · depth 21
• Kummer isomorphism for the mod p Selmer module, twisted NumberField.LevelArith.exists_selmerRep_linearEquiv_levelConstantHom 16 below · cited by 1 · depth 21
• Finiteness of the mod p S-unit, class and Selmer modules NumberField.LevelArith.finiteDimensional_unitsModP_sClass_selmerRep 2 below · cited by 2 · depth 21
• A[p] ≅ A/pA as ℤ/p-representations when p ∤ |G| NumberField.LevelArith.nonempty_repTorsionP_iso_repModP 1 below · cited by 2 · depth 21
• S-prime classes: Galois-stable part equals the closure NumberField.LevelArith.sPrimeClasses_eq_closure 0 below · cited by 4 · depth 21
• Galois stability of the maximal S-unit group NumberField.LevelArith.sUnitsMaxStable_eq_sUnitsMax 0 below · cited by 13 · depth 21
• Galois-stable Selmer subgroup equals the Selmer group NumberField.LevelArith.selmerStable_eq_selmer 0 below · cited by 2 · depth 21
• Capitulation of p-power ideals in levels unramified outside S NumberField.LevelArith.exists_isUnramifiedOutside_map_isPrincipal_of_pow_eq_span 6 below · cited by 2 · depth 22
• Every continuous ℤ/p-character is a Kummer character NumberField.LevelArith.exists_kummerChar_eq_of_continuous 4 below · cited by 1 · depth 22
• Inertia above w ∤ p fixes p-th roots NumberField.LevelArith.inertia_apply_eq_of_dvd_valuation 0 below · cited by 4 · depth 22
• Conjugation rule for the Kummer character: cyclotomic twist NumberField.LevelArith.kummerChar_conj_eq_cycloChar_mul 0 below · cited by 1 · depth 22
• Vanishing of the Kummer character detects p-th powers NumberField.LevelArith.kummerChar_eq_zero_iff 0 below · cited by 1 · depth 22
• Level-constancy of the Kummer character via divisibility of valuations NumberField.LevelArith.kummerChar_isLevelConstant_iff_forall_dvd_valuation 7 below · cited by 1 · depth 22
• Kummer character: bi-additive and trivial on Gal(ℚ̄/F(y)) NumberField.LevelArith.kummerChar_mul_and_add_and_level 0 below · cited by 2 · depth 22
• Mod p torsion of the S-units is 𝔽ₚ(1) NumberField.LevelArith.nonempty_repTorsionP_sUnitsMaxRep_iso_trivial_twist_cycloChar 2 below · cited by 2 · depth 22
• Smoothness and p-divisibility of the S-unit module NumberField.LevelArith.sUnitsMaxRep_smooth_and_divisible 2 below · cited by 3 · depth 22
• Naturality of Brauer local invariants under automorphisms of L NumberField.LevelArith.apply_eq_apply_of_isBrauerLocalInv_of_algEquiv 125 below · cited by 1 · depth 23
• Cochain identities descend along inflation to a layer NumberField.LevelArith.d_eq_zero_and_d_eq_pow_smul_of_level_presentation_sUnitsMaxRep 0 below · cited by 1 · depth 23
• Existence of a local invariant map on p-primary H²_S NumberField.LevelArith.exists_isBrauerLocalInv 152 below · cited by 1 · depth 23
• Inflating a layer coboundary to a level-constant 2-cochain NumberField.LevelArith.exists_isLevelConstant_d_two_three_eq_of_level_coboundary_sUnitsMaxRep 0 below · cited by 1 · depth 23
• Inflating a layer cochain to a larger layer NumberField.LevelArith.exists_level_comp_eq_of_le_sUnitsMaxRep 0 below · cited by 1 · depth 23
• Presenting a level-constant cochain at a finite Galois level NumberField.LevelArith.exists_level_eq_comp_of_isLevelConstant_sUnitsMaxRep 5 below · cited by 1 · depth 23
• Inflation kills p-power-torsion 3-cocycles of S-units NumberField.LevelArith.exists_level_inhomogeneousCochains_d_two_three_eq_of_pow_smul 480 below · cited by 1 · depth 23
• Inertia above w moves a p-th root when p ∤ v_w(x) NumberField.LevelArith.exists_valuationSubring_inertia_apply_ne_of_not_dvd_valuation 3 below · cited by 1 · depth 23
• Reciprocity for p-primary S-ramified classes over L NumberField.LevelArith.finsum_apply_eq_zero_of_isBrauerLocalInv 403 below · cited by 1 · depth 23
• Injectivity of any Brauer local-invariant map on p-primary classes NumberField.LevelArith.injective_of_isBrauerLocalInv 280 below · cited by 1 · depth 23
• Realisation of sum-zero p-primary families of local invariants NumberField.LevelArith.mem_range_of_isBrauerLocalInv_of_finsum_eq_zero 422 below · cited by 1 · depth 23
• Inflation kills p-primary S-unit classes with vanishing idèle image NumberField.LevelArith.continuousH2SrInflation_H2pi_eq_zero_of_map_principalIdele_eq_zero_of_pow_smul_eq_zero 162 below · cited by 1 · depth 24
• Uniqueness of the Brauer local invariant at a place NumberField.LevelArith.eq_of_hasBrauerLocalInvAt 146 below · cited by 1 · depth 24
• Invariants of the maximal S-units are the S-units of F NumberField.LevelArith.exists_addEquiv_quotientToInvariants_sUnitsMaxRep_sUnitsRep 7 below · cited by 3 · depth 24
• Conjugating an inflated level 2-cocycle by σ NumberField.LevelArith.exists_cocyclesTwo_conj_transport_continuousH2SrInflation_eq 4 below · cited by 1 · depth 24
• Brauer class with prescribed invariants from an idèle class NumberField.LevelArith.exists_forall_hasBrauerLocalInvAt_of_ideleClass_hasLocalInv 175 below · cited by 1 · depth 24
• Existence of a local Brauer invariant at a place above S NumberField.LevelArith.exists_hasBrauerLocalInvAt 118 below · cited by 2 · depth 24
• One layer presentation for a p-primary H²_S class NumberField.LevelArith.exists_layer_presentation_and_pow_smul_eq_zero 18 below · cited by 2 · depth 24
• Existence of a Sylow intermediate field for a finite layer NumberField.LevelArith.exists_le_le_isPGroup_quotient_not_dvd_finrank 1 below · cited by 3 · depth 24
• Capitulation at a larger level of S-unit 2-cocycles NumberField.LevelArith.exists_level_coboundary_of_isPGroup_of_map_diag_H2pi_eq_zero_sUnitsMaxRep 143 below · cited by 3 · depth 24
• Prime-to-p descent of degree-3 S-unit coboundaries NumberField.LevelArith.exists_level_d_two_three_eq_of_restrict_coboundary_of_not_dvd 3 below · cited by 2 · depth 24
• Realising p-primary sum-zero families as local invariants of idèle classes NumberField.LevelArith.exists_level_ideleClass_hasLocalInv_of_finsum_eq_zero 385 below · cited by 1 · depth 24
• Killing a degree-three S-unit cocycle at a deeper level NumberField.LevelArith.exists_level_inhomogeneousCochains_d_two_three_eq_of_pow_smul_of_isPGroup 479 below · cited by 1 · depth 24
• Invariant maximal S-units as the S-units of F NumberField.LevelArith.exists_monoidHom_levelGal_exists_hom_res_quotientToInvariants_sUnitsRep_bijective 8 below · cited by 11 · depth 24
• Restriction of degree-3 S-unit cochain data to a larger base NumberField.LevelArith.exists_three_cochain_val_eq_of_le_sUnitsMaxRep 1 below · cited by 2 · depth 24
• Additivity of Brauer local invariants at a place NumberField.LevelArith.hasBrauerLocalInvAt_add 144 below · cited by 1 · depth 24
• Local w-components of σ-transported H² classes agree NumberField.LevelArith.map_prG_conj_transport_eq_map_prG_map_psi 1 below · cited by 1 · depth 24
• Local component at w ∤ S of an S-unit class vanishes NumberField.LevelArith.map_prG_map_principalIdele_eq_zero_of_forall_comap_ne 22 below · cited by 2 · depth 24
• Unramifiedness off S of the layer F_L over L NumberField.LevelArith.ramificationIdx_eq_one_of_isUnramifiedOutside_of_under_not_mem_placesOverPrimesFinset 6 below · cited by 3 · depth 24
• Inflated p-primary class vanishes after prime-to-p restriction NumberField.LevelArith.continuousH2SrInflation_H2pi_eq_zero_of_restrict_coboundary_of_not_dvd 7 below · cited by 1 · depth 25
• Trivial decomposition at infinity in a p-group layer NumberField.LevelArith.eq_one_of_mem_infPlaceDecomp_of_isPGroup 1 below · cited by 3 · depth 25
• Archimedean local splitting of an S-unit 2-cocycle NumberField.LevelArith.exists_coboundary_localUnits_infinitePlace_of_forall_conj_archimedeanDecomposition 0 below · cited by 1 · depth 25
• Restricting an S-unit 2-cocycle to a larger base field NumberField.LevelArith.exists_cocyclesTwo_quotientToInvariants_sUnitsMaxRep_val_eq_of_le 1 below · cited by 1 · depth 25
• Presenting a p-primary S-Brauer class with prescribed local invariants NumberField.LevelArith.exists_forall_hasBrauerLocalInvAt_of_cocycles_sUnitsRep 1 below · cited by 1 · depth 25
• Vanishing of H³ of the S-idèle module of a level NumberField.LevelArith.exists_inhomogeneousCochains_d_two_three_eq_sIdele 158 below · cited by 2 · depth 25
• Galois S-levels with p^k-divisible local degrees above S NumberField.LevelArith.exists_isUnramifiedOutside_isGalois_pow_dvd_natCard_decomp 11 below · cited by 2 · depth 25
• Local coboundaries yield a coboundary in an adic completion NumberField.LevelArith.exists_layer_coboundary_adicCompletion_of_forall_conj_primeLocal_coboundary 9 below · cited by 1 · depth 25
• Degree-3 S-unit cocycles split at a deeper p-level NumberField.LevelArith.exists_level_d_two_three_eq_of_sIdele_coboundary_of_isPGroup 478 below · cited by 1 · depth 25
• Cocycles with equal inflated class differ by a coboundary at a deeper level NumberField.LevelArith.exists_level_sub_eq_coboundary_of_continuousH2SrInflation_eq 4 below · cited by 1 · depth 25
• Transporting a degree-3 cochain to the S-units frame NumberField.LevelArith.exists_three_cochain_sUnitsRep_val_eq_of_transport 0 below · cited by 2 · depth 25
• Local invariants unchanged on passing to a larger S-level NumberField.LevelArith.hasLocalInv_of_hasLocalInv_of_le 119 below · cited by 2 · depth 25
• The layer F_L/L is Galois for F/ℚ finite normal NumberField.LevelArith.isGalois_levelField 0 below · cited by 8 · depth 25
• Surjectivity and kernel of Γ_L → Gal(F/L) NumberField.LevelArith.levelGal_surjective_and_ker 0 below · cited by 12 · depth 25
• Vanishing S-idèle class of a restricted layer 2-cocycle NumberField.LevelArith.map_diag_H2pi_eq_zero_of_map_principalIdele_H2pi_eq_zero_of_le 30 below · cited by 1 · depth 25
• Layer order p^k kills degree-3 cocycles at cochain level NumberField.LevelArith.exists_card_eq_pow_and_d_two_three_eq_pow_smul_of_isPGroup 1 below · cited by 1 · depth 26
• Galois S-levels above a given level with p^k dividing decomposition orders NumberField.LevelArith.exists_le_isUnramifiedOutside_isGalois_pow_dvd_natCard_decomp 12 below · cited by 1 · depth 26
• Depth splitting of a 3-cocycle of S-units NumberField.LevelArith.exists_level_d_two_three_eq_of_sIdele_coboundary_of_smul_eq_of_dvd_natCard_decomp 415 below · cited by 1 · depth 26
• Sylow placement of a large decomposition group NumberField.LevelArith.exists_mem_placesOverPrimesFinset_pow_dvd_natCard_decomp_above_of_isPGroup_of_not_dvd 6 below · cited by 1 · depth 26
• Torsion transfer of S-idèle cochains along a level tower NumberField.LevelArith.exists_smul_eq_smul_add_d_add_diag_of_sIdele_coboundary_of_le 43 below · cited by 1 · depth 26
• Inflation of degree-3 cochain data to a larger layer NumberField.LevelArith.exists_three_cochain_val_eq_of_le_level_sUnitsMaxRep 0 below · cited by 1 · depth 26
• Vanishing idèle class transfers from base L to L' NumberField.LevelArith.map_principalIdele_H2pi_eq_zero_of_le 2 below · cited by 1 · depth 26
• Capitulation step: idèlic 2-cochain gives deeper S-unit coboundary NumberField.LevelArith.exists_level_sUnitsRep_val_d_eq_of_sIdele_coboundary_of_map_eq_add_d 56 below · cited by 1 · depth 27
• Change of base field within a fixed layer F NumberField.LevelArith.exists_ringEquiv_monoidHom_equiv_heightOneSpectrum_levelField_of_le_le 1 below · cited by 1 · depth 27
• Un-transporting a degree-3 coboundary to the invariants frame NumberField.LevelArith.exists_two_cochain_quotientToInvariants_sUnitsMaxRep_eq_d_of_transport 0 below · cited by 1 · depth 27
• Γ_L/U_F a p-group forces Gal(F_L/L) a p-group NumberField.LevelArith.isPGroup_levelGal_of_isPGroup_quotient 1 below · cited by 2 · depth 27
• Genuine base change preserves S-idèles and S-units in level towers NumberField.LevelArith.unitsMap_genuineBaseChange_mem_unitIdelesOutside_of_le 2 below · cited by 2 · depth 27
• A Galois S-level absorbing p-power idèle classes NumberField.LevelArith.exists_le_unitsMap_genuineBaseChange_mem_sup_of_pow_mem 14 below · cited by 1 · depth 28

NumberField.NormIndex 2

• Idelic norm containing the unit ideles of an admissible modulus NumberField.NormIndex.ideleFirstIneqData_unitIdeles_le_range_of_isCyclic_of_finrank_dvd 65 below · cited by 1 · depth 16
• Admissibility of a modulus descends to divisors of the degree NumberField.NormIndex.IsAdmissibleModulusOfDegree.of_dvd_degree 0 below · cited by 1 · depth 17

NumberField.PlaceDecomp 71

• Restriction of decomposition groups in a tower of number fields NumberField.PlaceDecomp.exists_restrict_decomp_surjective_of_tower 1 below · cited by 19 · depth 14
• Herbrand's theorem in functional form along a tower NumberField.PlaceDecomp.finsum_card_lowerRamificationGroup_mul_apply_map_eq_of_restrict 21 below · cited by 1 · depth 14
• Faithfulness of the decomposition group action on K_w NumberField.PlaceDecomp.faithfulSMul_decomp 1 below · cited by 22 · depth 15
• Completion preserves the lower ramification filtration NumberField.PlaceDecomp.lowerRamificationGroup_valuationSubring_eq_adicCompletionIntegers 0 below · cited by 3 · depth 15
• The different is local at each prime of a Galois extension NumberField.PlaceDecomp.map_differentIdeal_valuationSubring_eq_differentIdeal_fixedPoints 4 below · cited by 1 · depth 15
• Lower ramification groups of a quotient decomposition group NumberField.PlaceDecomp.map_lowerRamificationGroup_fixedPoints_adicCompletionIntegers_eq_of_restrict 6 below · cited by 3 · depth 15
• Decomposition group fixes exactly the lower completion NumberField.PlaceDecomp.forall_smul_eq_iff_mem_range_adicCompletionSemialgHom 4 below · cited by 16 · depth 16
• Order of the decomposition group equals ef NumberField.PlaceDecomp.natCard_decomp_eq_ramificationIdx_mul_inertiaDeg 1 below · cited by 10 · depth 16
• Decomposition-group action on K_w extends that on K NumberField.PlaceDecomp.smul_algebraMap 0 below · cited by 6 · depth 16
• Local norm index via carry classes in H²(D_w, F_w^×) NumberField.PlaceDecomp.exists_carryClassHom_surjective_ker_eq_norms_adicCompletion 101 below · cited by 3 · depth 18
• Local norm index bound for abelian decomposition group NumberField.PlaceDecomp.exists_fin_forall_exists_finprod_smul_eq_mul_of_isMulCommutative_decomp 107 below · cited by 1 · depth 18
• Level-n units of Eᵥ are norms from the Gⁿ layer NumberField.PlaceDecomp.exists_forall_upperRamificationGroup_smul_eq_and_finprod_quotient_smul_eq_of_valuation_sub_one_le 30 below · cited by 1 · depth 18
• A p-th root of q forces p ∣ |D_w| above q NumberField.PlaceDecomp.dvd_natCard_decomp_of_pow_eq_prime 2 below · cited by 1 · depth 19
• Equivariant q-adic bridge and local fundamental class at w NumberField.PlaceDecomp.exists_faithful_bridge_isBase_isLocalFundamentalClass 92 below · cited by 1 · depth 19
• Norm-coset representatives descend below the decomposition field NumberField.PlaceDecomp.exists_fin_forall_exists_finprod_smul_eq_mul_of_forall_smul_algebraMap_eq 6 below · cited by 1 · depth 19
• Cyclic decomposition group: local norm index at most |D_w| NumberField.PlaceDecomp.exists_fin_forall_exists_finprod_smul_eq_mul_of_isCyclic_decomp 102 below · cited by 1 · depth 19
• Sub-multiplicativity of local norm classes in a tower NumberField.PlaceDecomp.exists_fin_mul_forall_exists_finprod_smul_eq_of_tower 6 below · cited by 1 · depth 19
• Higher units are norms from a prime-degree layer beyond the jump NumberField.PlaceDecomp.exists_finprod_smul_eq_of_valuation_sub_one_le_of_jump_lt_of_prime_card_decomp 10 below · cited by 1 · depth 19
• Local fundamental class for the decomposition group at w NumberField.PlaceDecomp.exists_fundamentalClass_units_adicCompletion 95 below · cited by 4 · depth 19
• Local coordinate at w∣ q of a descended Kummer class NumberField.PlaceDecomp.exists_int_map_res_kummer_eq_zsmul_and_localInv_locRes2S_eq 159 below · cited by 1 · depth 19
• Existence of a degree-one local bridge at a finite place NumberField.PlaceDecomp.exists_isLocalBridge1_padicAlgCl 17 below · cited by 2 · depth 19
• Completion at a finite place as a finite layer of ℚ̄_q NumberField.PlaceDecomp.exists_localLevel_ringEquiv_adicCompletion 0 below · cited by 14 · depth 19
• q-adic coordinates for a completion at a finite place NumberField.PlaceDecomp.exists_ringHom_adicCompletion_padicAlgCl_extends_padicEmbedding 1 below · cited by 4 · depth 19
• Idèle-class invariant at w equals the local Tate pairing NumberField.PlaceDecomp.exists_unit_inv_map_delta_res_eq_theta_localBridge 163 below · cited by 1 · depth 19
• Local invariant of the connecting map equals the Tate pairing NumberField.PlaceDecomp.exists_unit_inv_map_delta_res_eq_theta_localBridge_primary 163 below · cited by 2 · depth 19
• Local norm onto higher units at an unramified place NumberField.PlaceDecomp.forall_exists_finprod_smul_eq_and_of_ramificationIdx_eq_one 7 below · cited by 1 · depth 19
• Invariant at w of the descended class equals efm/p NumberField.PlaceDecomp.inv_map_lam_map_rho_res_eq_of_map_rho_res_eq_zsmul_of_forall_inv_eq 95 below · cited by 1 · depth 19
• Arithmetic hypotheses of the local bridge at a finite place NumberField.PlaceDecomp.localBridge_hypotheses_padicAlgCl 13 below · cited by 2 · depth 19
• Herbrand's theorem for upper ramification groups in a tower NumberField.PlaceDecomp.map_restrictNormalHom_upperRamificationGroup_eq 20 below · cited by 1 · depth 19
• Vanishing of the sum of local invariants over S NumberField.PlaceDecomp.sum_sum_inv_decomp_eq_zero_of_forall_inv_eq_of_isUnramifiedOutside 382 below · cited by 1 · depth 19
• Transitivity of the Herbrand function in a tower of number fields NumberField.PlaceDecomp.valuationSubring_herbrandPhi_eq_herbrandPhi_under_herbrandPhi 18 below · cited by 1 · depth 19
• Local norm as product over the decomposition group NumberField.PlaceDecomp.adicCompletionSemialgHom_norm_eq_finprod_smul 3 below · cited by 2 · depth 20
• Places above v times decomposition group equals #Gal(K/E) NumberField.PlaceDecomp.card_over_mul_card_decomp_above 0 below · cited by 2 · depth 20
• H²(D_w,K_w^×) is generated by the transported fundamental class NumberField.PlaceDecomp.exists_eq_zsmul_map_of_isLocalFundamentalClass 69 below · cited by 8 · depth 20
• Divisible lift to ℚ̄_q^× fixed by a finite global level NumberField.PlaceDecomp.exists_extension_fixed_of_injective_padicAlgCl 5 below · cited by 2 · depth 20
• Level-constant cocycles into ℚ̄_q^× are level-fixed coboundaries NumberField.PlaceDecomp.exists_fixed_d01_eq_of_isLevelConstant1_padicAlgCl 9 below · cited by 2 · depth 20
• Each σ cuts out a place of F above q NumberField.PlaceDecomp.exists_forall_mem_asIdeal_iff_norm_padicEmbedding_lt_one 0 below · cited by 1 · depth 20
• Compatible q-adic models of completions in a tower of places NumberField.PlaceDecomp.exists_localLevel_ringEquiv_adicCompletion_tower 2 below · cited by 4 · depth 20
• q-adic coordinates of F_w for a prescribed σ NumberField.PlaceDecomp.exists_ringHom_adicCompletion_padicAlgCl_of_forall_mem_asIdeal_iff 2 below · cited by 1 · depth 20
• Local bridge matches δ with a cup product up to a unit NumberField.PlaceDecomp.exists_unit_inflate_map_delta_res_eq_kummer_cup_localBridge_of_isLevelConstant 0 below · cited by 2 · depth 20
• Existence of a universal unit normalising the local invariant NumberField.PlaceDecomp.exists_unit_localInv_eq_mul_of_inflate_eq_kummer 149 below · cited by 2 · depth 20
• Units fixed by the kernel lie in Φ(F_w^×) NumberField.PlaceDecomp.exists_unit_map_eq_of_forall_apply_eq_padicAlgCl 1 below · cited by 2 · depth 20
• Sum of local invariants of a global class vanishes NumberField.PlaceDecomp.finsum_inv_decomp_above_map_lam_rho_res_eq_zero_of_isPGroup_of_ne_two 377 below · cited by 1 · depth 20
• Local invariant equals m for a Kummer-inflated fundamental class NumberField.PlaceDecomp.localInv_eq_of_inflate_eq_kummer 148 below · cited by 2 · depth 20
• Bridge-independence of the local fundamental class at w NumberField.PlaceDecomp.map_eq_map_of_isLocalFundamentalClass_of_ringEquiv_adicCompletion 92 below · cited by 9 · depth 20
• Vanishing local coordinate at an unramified place NumberField.PlaceDecomp.map_map_res_H2_units_eq_zero_of_isOfFinOrder_of_ramificationIdx_eq_one 15 below · cited by 1 · depth 20
• A ring isomorphism F_w ≅ L' detects integers and residue characteristic NumberField.PlaceDecomp.mem_adicCompletionIntegers_iff_norm_le_one_and_natCast_mem_asIdeal_of_ringEquiv 0 below · cited by 12 · depth 20
• A continuous q-adic embedding of F_w recovers w NumberField.PlaceDecomp.mem_asIdeal_iff_norm_padicEmbedding_lt_one_of_continuous 0 below · cited by 1 · depth 20
• Decomposition group over ℚ versus over an intermediate field NumberField.PlaceDecomp.natCard_decomp_eq_ramificationIdx_mul_inertiaDeg_mul_natCard_decomp 2 below · cited by 1 · depth 20
• Order of the transported local fundamental class in H²(D_w,K_w^×) NumberField.PlaceDecomp.zsmul_map_eq_zero_iff_natCard_decomp_dvd_of_isLocalFundamentalClass 67 below · cited by 8 · depth 20
• Places of K^H above S count H-orbits on coprodᵥ G/Dᵥ NumberField.PlaceDecomp.card_over_fixedField_eq_card_orbitRel_quotient 0 below · cited by 1 · depth 21
• Tate cohomology of local units in cyclic degrees 0 and -1 NumberField.PlaceDecomp.card_tateH0_units_eq_card_and_subsingleton_tateHneg1 14 below · cited by 2 · depth 21
• Trivial inertia action on 𝒪_w forces σ = 1 when e = 1 NumberField.PlaceDecomp.decomp_eq_one_of_ramificationIdx_eq_one 1 below · cited by 4 · depth 21
• Local fundamental classes along a tower of decomposition groups NumberField.PlaceDecomp.exists_isLocalFundamentalClass_map_eq_natCard_ker_smul_of_tower 86 below · cited by 2 · depth 21
• Degree formula for place sums in ℚ/ℤ NumberField.PlaceDecomp.finsum_div_natCard_decomp_eq_finrank_smul_finsum 2 below · cited by 2 · depth 21
• Inflated local class equals inflated carry cocycle modulo coboundaries NumberField.PlaceDecomp.inflate_sub_unitsInflate2_carryFun_mem_levelCoboundaries2 101 below · cited by 1 · depth 21
• Tate cohomology of local units vanishes at unramified places NumberField.PlaceDecomp.subsingleton_tateCohomology_integerUnits_of_ramificationIdx_eq_one 14 below · cited by 5 · depth 21
• Vanishing Tate cohomology of local units at unramified places NumberField.PlaceDecomp.subsingleton_tate_integerUnits_of_unramified 8 below · cited by 2 · depth 21
• Conjugation and transport for H-decomposition groups at conjugate places NumberField.PlaceDecomp.exists_conj_and_transport_repHom_inf_decomp_of_smul_eq 3 below · cited by 1 · depth 22
• Conjugate places: decomposition groups and transport of local units NumberField.PlaceDecomp.exists_conj_and_transport_repHom_of_smul_eq 3 below · cited by 5 · depth 22
• Conjugation transport of local unit representations along g w₁ = w NumberField.PlaceDecomp.exists_conj_subgroupOf_and_transport_repHom_of_smul_eq 3 below · cited by 1 · depth 22
• Restricted local fundamental class generates H²(H∩ D_w,K_w^×) NumberField.PlaceDecomp.exists_eq_zsmul_map_inclusion_and_zsmul_eq_zero_iff_of_isLocalFundamentalClass 71 below · cited by 1 · depth 22
• Restriction of the transported local fundamental class generates H²(S,K_w^×) NumberField.PlaceDecomp.exists_eq_zsmul_map_subtype_and_zsmul_eq_zero_iff_of_isLocalFundamentalClass 69 below · cited by 2 · depth 22
• Local fundamental classes above every finite place NumberField.PlaceDecomp.exists_forall_isLocalFundamentalClass_above 92 below · cited by 5 · depth 22
• Transport of a local fundamental class along σ NumberField.PlaceDecomp.exists_isLocalFundamentalClass_map_eq_map_of_smul_eq 3 below · cited by 3 · depth 22
• Decomposition group at w as Aut of the completion NumberField.PlaceDecomp.exists_mulEquiv_decompositionSubgroup_fixedPoints 3 below · cited by 2 · depth 22
• Decomposition subgroups at finite places generate a cyclic Galois group NumberField.PlaceDecomp.iSup_decomp_eq_top_of_isCyclic 135 below · cited by 1 · depth 22
• Unramified decomposition group is cyclic NumberField.PlaceDecomp.isCyclic_decomp_of_ramificationIdx_eq_one 3 below · cited by 1 · depth 22
• Every automorphism over the fixed field stabilises mathcal O_w NumberField.PlaceDecomp.decompositionSubgroup_fixedPoints_eq_top 0 below · cited by 1 · depth 23
• Decomposition group orders in a tower of Galois number fields NumberField.PlaceDecomp.natCard_decomp_eq_mul_and_natCard_inf_decomp_dvd_of_dvd 2 below · cited by 1 · depth 24
• Vanishing of H³(D_w, (K_w)^×) at cochain level NumberField.PlaceDecomp.exists_inhomogeneousCochains_d_two_three_eq_adicCompletion 136 below · cited by 1 · depth 26

NumberField.PlaceTransport 11

• Stabiliser of a finite place equals its decomposition subgroup NumberField.PlaceTransport.stabilizer_eq_decomp 0 below · cited by 29 · depth 15
• Galois orbits of finite places are the fibres of `under` NumberField.PlaceTransport.orbit_eq_setOf_under_eq 0 below · cited by 22 · depth 19
• Place transport commutes with the canonical embeddings Eᵥ → K_w NumberField.PlaceTransport.transport_adicCompletionSemialgHom 0 below · cited by 3 · depth 19
• Conjugation by Aut(K/E) fixes the place below NumberField.PlaceTransport.under_smul 0 below · cited by 18 · depth 19
• Places above S as a disjoint union of coset spaces NumberField.PlaceTransport.exists_equiv_placesAbove_sigma_quotient_decomp_above 2 below · cited by 1 · depth 20
• Transport along σ agrees with the decomposition-group action on K_w NumberField.PlaceTransport.transport_eq_actRingEquiv 0 below · cited by 11 · depth 20
• Composition law for transport of adic completions along conjugation NumberField.PlaceTransport.transport_trans_transport 0 below · cited by 13 · depth 20
• Transport along the identity automorphism is the identity NumberField.PlaceTransport.transport_one 0 below · cited by 6 · depth 21
• Places above v in F^H and double cosets D_wbackslash G/H NumberField.PlaceTransport.exists_bijective_doubleCoset_decomp_of_under_eq 3 below · cited by 1 · depth 22
• A Sylow p-subgroup meets some conjugate decomposition group deeply NumberField.PlaceTransport.exists_pow_dvd_natCard_inf_decomp_smul_of_isPGroup_of_not_dvd_index 1 below · cited by 1 · depth 27
• Cyclic Galois group moves places above v by a natural power NumberField.PlaceTransport.exists_pow_smul_eq_of_forall_mem_zpowers 0 below · cited by 3 · depth 32

NumberField.PrimeNormIndex 7

• Ray-class character trivial on norms factors through the Artin symbol NumberField.PrimeNormIndex.normClassChar_eq_char_comp_artinSymbol 0 below · cited by 1 · depth 15
• Second inequality for Galois cubic extensions NumberField.PrimeNormIndex.secondInequalityCTM_of_finrank_eq_three 101 below · cited by 1 · depth 16
• Idelic first-inequality data for a prime-degree Galois extension NumberField.PrimeNormIndex.ideleFirstIneqDataAt_of_finrank_eq_prime 64 below · cited by 2 · depth 17
• Second inequality at prime degree, no roots of unity assumed NumberField.PrimeNormIndex.secondInequalityCTM_of_finrank_eq_prime 99 below · cited by 2 · depth 17
• Second inequality for a prime Kummer layer NumberField.PrimeNormIndex.secondInequalityCTM_of_primitiveRoots 98 below · cited by 2 · depth 17
• Second inequality in prime degree: norm-coset index divides p NumberField.PrimeNormIndex.ideleClass_normCoset_index_dvd_of_finrank_eq_prime 104 below · cited by 2 · depth 21
• Second inequality at prime degree: ̂ H⁰ of idele classes NumberField.PrimeNormIndex.ideleClassGroup_tateCard_zero_dvd_of_finrank_eq_prime 107 below · cited by 1 · depth 24

NumberField.QuadraticNormIndex 1

• Quadratic norm-class characters: triviality or residue-degree dichotomy NumberField.QuadraticNormIndex.normClassChar_eq_one_or_inertiaDeg_iff 0 below · cited by 1 · depth 16

NumberField.SArchIdele 3

• Unique equivariant map of S∪∞-idèle modules along a tower NumberField.SArchIdele.existsUnique_hom_res_obj_comp_toSIdele_eq 3 below · cited by 2 · depth 19
• Exactness at the S∪∞-idèle module NumberField.SArchIdele.toSIdeleClass_mk_comp_diagS_eq_one_and_exists_of_eq_one 2 below · cited by 2 · depth 19
• Image of the S∪∞-idèle module in the idèles NumberField.SArchIdele.injective_comp_toSIdele_and_mem_range_iff 2 below · cited by 1 · depth 20

NumberField.SIdele 11

• Coordinatewise equivariant embedding of the S-idèle module NumberField.SIdele.exists_addMonoidHom_obj_adeleRing_units_apply 17 below · cited by 6 · depth 19
• Semilocal description of S-idèle cohomology in positive degree NumberField.SIdele.bijective_groupCohomology_localCoordinates_of_ramificationIdx_eq_one 16 below · cited by 4 · depth 23
• Local coordinate at v vanishes for a layer coboundary NumberField.SIdele.localCoordinate_map_diag_H2pi_eq_zero_of_exists_layer_coboundary 104 below · cited by 1 · depth 25
• The S-idèle module as a Galois-equivariant embedding into the idèles NumberField.SIdele.exists_hom_obj_ideles_injective_of_ideleGaloisDescent 18 below · cited by 2 · depth 26
• Injectivity on H² of the S-idèle inclusion NumberField.SIdele.injective_map_H2_of_injective_of_range_eq_unitIdelesOutside 11 below · cited by 1 · depth 26
• Idèle classes trivial off S descend uniquely to S-idèles NumberField.SIdele.existsUnique_map_eq_of_forall_map_prG_eq_zero 12 below · cited by 1 · depth 27
• S-idèle class module embeds into the idèle class group NumberField.SIdele.exists_hom_classObj_ideleClassGroup_injective_range_eq 21 below · cited by 3 · depth 27
• Equivariance of Φ upgraded to a morphism of representations NumberField.SIdele.exists_hom_ideles_apply_eq 0 below · cited by 2 · depth 27
• Torsion for S-idèle 2-cochains modulo S-units NumberField.SIdele.exists_smul_eq_d_add_diag_of_d_eq_diag 7 below · cited by 1 · depth 27
• Equivariant realisation of the S-idèle module inside A_K^× NumberField.SIdele.exists_addMonoidHom_obj_adeleRing_units 18 below · cited by 1 · depth 28
• S-idèle module realised inside the idèle group NumberField.SIdele.exists_addMonoidHom_obj_adeleRing_units_transport 12 below · cited by 1 · depth 29

NumberField.SUnits 14

• Extending an S-unit map to P with S-level values NumberField.SUnits.exists_ihom_extension_fixed_of_sLevel_of_injective 2 below · cited by 5 · depth 19
• Cocycles inflated from F lie in the image of Λ_E NumberField.SUnits.exists_isGlobalBridge2_apply_eq_continuousH2Spi_of_forall_mul_eq 8 below · cited by 1 · depth 19
• Kernel of the global degree-two bridge dies under inflation NumberField.SUnits.exists_level_forall_map_extInflR_eq_zero_of_isGlobalBridge2_apply_eq_zero 48 below · cited by 1 · depth 19
• Inflation invariance of the global degree-two bridge Λ_E NumberField.SUnits.isGlobalBridge2_apply_inflation_eq 3 below · cited by 2 · depth 19
• Localisation of the degree-two global bridge at a finite place NumberField.SUnits.locRes2S_isGlobalBridge2_apply_eq_of_finite 7 below · cited by 1 · depth 19
• S-units are units at valuation rings over primes outside S NumberField.SUnits.algebraMap_mem_and_inv_mem_of_mem_sUnits_of_liesOverPrime 0 below · cited by 4 · depth 20
• An S-level making S-units of F₁ into p-th powers NumberField.SUnits.exists_sLevel_forall_sUnitsRep_map_val_eq_pow 13 below · cited by 1 · depth 20
• Equivariant mod-p S-unit rank identity with coefficients NumberField.SUnits.finrank_invariants_repModP_sUnitsRep_tensor_add 28 below · cited by 1 · depth 20
• Global degree-two bridge on the defect class equals the inflated cocycle NumberField.SUnits.isGlobalBridge2_apply_map_homSeq_f_eq_continuousH2Spi_of_eq_delta 0 below · cited by 2 · depth 20
• Local-bridge classes of S-units lie in continuousH1S NumberField.SUnits.isLocalBridge1_apply_mem_continuousH1S 2 below · cited by 1 · depth 20
• Local–global compatibility of the degree-one bridges at q NumberField.SUnits.locRes_isLocalBridge1_apply_eq_of_finite 0 below · cited by 1 · depth 20
• Finite generation of the S-unit Galois representation NumberField.SUnits.moduleFinite_sUnitsRep 2 below · cited by 1 · depth 20
• Galois-invariant S-units are all S-units NumberField.SUnits.sUnits_eq_unit 0 below · cited by 8 · depth 20
• Rank of the H-invariant S-units of K NumberField.SUnits.finrank_groupCohomology_zero_sUnitsRep_add_one 2 below · cited by 1 · depth 21

NumberField.StandardAddChar 10

• The standard adelic character ψ_F is global NumberField.StandardAddChar.isGlobalAddChar_stdAddChar 0 below · cited by 59 · depth 14
• Archimedean normalisation of the standard adelic character NumberField.StandardAddChar.stdAddChar_apply_mk_zero_eq_fourierChar_trace 2 below · cited by 12 · depth 16
• Archimedean component of the standard adelic character NumberField.StandardAddChar.AdelicTraceData.psiK_apply_mk_zero_eq_fourierChar_trace 1 below · cited by 1 · depth 17
• Local standard character and the local trace NumberField.StandardAddChar.psiLocal_eq_psiLocal_trace 1 below · cited by 6 · depth 17
• Local component at v of the standard adelic character of ℚ NumberField.StandardAddChar.psiLocal_rat_eq_psiV 0 below · cited by 38 · depth 17
• Local standard character of ℚₚ equals ψ_ℚ NumberField.StandardAddChar.psiLocal_rat_eq_psiQ_adeleSingleAt 0 below · cited by 8 · depth 19
• Standard adelic character on the line of a real place NumberField.StandardAddChar.stdAddChar_single_infinitePlace_of_isReal 0 below · cited by 6 · depth 19
• Indicator of 1+mathfrak pᵥⁿ as a finite character sum NumberField.StandardAddChar.exists_sum_mul_stdAddChar_mul_eq_indicator_one_add_pow 6 below · cited by 3 · depth 21
• Standard adelic character on the line of a complex place NumberField.StandardAddChar.stdAddChar_single_infinitePlace_of_isComplex 0 below · cited by 2 · depth 23
• Non-vanishing derivative at 0 of s↦ψ_ℚ(ι(s),0) NumberField.StandardAddChar.exists_ne_zero_and_hasDerivAt_psiQ_ofReal 0 below · cited by 1 · depth 29

NumberField.TateGlobal 96

• Continuity of the idelic norm on A_F^× NumberField.TateGlobal.continuous_ideleNorm 0 below · cited by 217 · depth 15
• Idele norm of a uniformizer idele is (Nv)⁻¹ NumberField.TateGlobal.ideleNorm_uniformizerIdele 2 below · cited by 49 · depth 15
• Fujisaki's theorem: compactness of the norm-one idele class group NumberField.TateGlobal.compactSpace_normOneIdeleClass 3 below · cited by 18 · depth 16
• Continuity of the idele norm of the determinant on adelic GL₂ NumberField.TateGlobal.continuous_ideleNorm_det 1 below · cited by 163 · depth 16
• Continuity of the local component at v of a continuous idele class character NumberField.TateGlobal.continuous_localChar 0 below · cited by 41 · depth 16
• A continuous idele character is unramified outside a finite set NumberField.TateGlobal.exists_finset_forall_isUnramifiedCharAt_of_continuous 0 below · cited by 32 · depth 16
• Tempered measurable fundamental domain for the principal ideles NumberField.TateGlobal.exists_isFundamentalDomain_principalIdeles_forall_exists_integrableOn_min_ideleNorm_pow 9 below · cited by 43 · depth 16
• Continuous characters separate points of C_F¹ NumberField.TateGlobal.forall_ne_one_exists_continuous_monoidHom_normOneIdeleClass_apply_ne_one 0 below · cited by 3 · depth 16
• Idele norm of det X for integral finite part NumberField.TateGlobal.ideleNorm_det_eq_prod_archDetNorm_pow_mult 2 below · cited by 71 · depth 16
• Idele norm one for integral ideles with trivial archimedean part NumberField.TateGlobal.ideleNorm_eq_one_of_fst_eq_one_of_finitePartUnits_mem_unitIdeles 2 below · cited by 55 · depth 16
• Local component of a character twisted by the idelic norm NumberField.TateGlobal.localChar_mul_comp_idelicNorm_genuineBaseChange 2 below · cited by 21 · depth 16
• Convergence and holomorphy of a partial degree-two Euler product NumberField.TateGlobal.differentiableOn_tprod_eulerFactor_of_norm_le_rpow 1 below · cited by 2 · depth 17
• A continuous homomorphic section of the idele norm NumberField.TateGlobal.exists_continuous_monoidHom_ideleNorm_apply_eq 0 below · cited by 57 · depth 17
• Entire partial Euler product for a non-trivial idele class character NumberField.TateGlobal.exists_differentiable_eq_partialEulerProduct_of_exists_mem_normOneIdeles_ne_one 50 below · cited by 10 · depth 17
• Unitary ideles characters trivial on A¹ are ‖·‖^{it} NumberField.TateGlobal.exists_eq_normPowChar_of_forall_mem_normOneIdeles 45 below · cited by 26 · depth 17
• Surjectivity of the idele norm onto ℝ_{>0}, with trivial finite part NumberField.TateGlobal.exists_ideleNorm_eq_and_snd_eq_one 4 below · cited by 51 · depth 17
• Absolute value of a continuous idele class character is a power of the idelic norm NumberField.TateGlobal.exists_norm_apply_eq_ideleNorm_rpow 5 below · cited by 42 · depth 17
• Unramified Euler coefficient of ‖·‖^{it} at v is Nv^{-it} NumberField.TateGlobal.ite_isUnramifiedCharAt_normPowChar_apply_uniformizerIdele_eq_absNorm_cpow_neg 4 below · cited by 20 · depth 17
• Determinant-norm slabs in GL₂(A_F) are Borel NumberField.TateGlobal.measurableSet_setOf_ideleNorm_det_mem_Icc 2 below · cited by 86 · depth 17
• Non-vanishing at s=1 of partial Hecke L-products NumberField.TateGlobal.not_tendsto_partialEulerProduct_nhds_zero_of_isUnitaryChar 66 below · cited by 5 · depth 17
• Idele character unramified outside S kills units away from S NumberField.TateGlobal.apply_eq_one_of_forall_isUnramifiedCharAt_of_continuous 0 below · cited by 15 · depth 18
• Non-vanishing at s=1 for a quadratic idele class character NumberField.TateGlobal.apply_one_ne_zero_of_differentiable_of_eq_partialEulerProduct_of_sq_eq_one 5 below · cited by 1 · depth 18
• Idele norm of an idele with trivial finite component NumberField.TateGlobal.ideleNorm_eq_prod_norm_infinitePlace_pow_mult_of_snd_eq_one 3 below · cited by 73 · depth 18
• Entire Mellin transforms over tempered regions of the ideles NumberField.TateGlobal.integrableOn_and_differentiable_setIntegral_mul_ideleNorm_cpow_of_norm_le_min_pow 1 below · cited by 1 · depth 18
• Integrability of Tate's global zeta integrand for Re s>1 NumberField.TateGlobal.integrable_zetaIntegrand 0 below · cited by 7 · depth 18
• Entire continuation and functional equation of Tate's zeta integral NumberField.TateGlobal.zetaIntegral_entire_continuation_fe_norm_le_of_re_mem_Icc_of_exists_mem_normOneIdeles_ne_one 45 below · cited by 3 · depth 18
• Entire continuation and functional equation of Tate's zeta integral NumberField.TateGlobal.zetaIntegral_entire_continuation_fe_of_exists_mem_normOneIdeles_ne_one 45 below · cited by 1 · depth 18
• Euler factorisation of Tate's global zeta integral outside S NumberField.TateGlobal.zetaIntegral_mul_eulerFactors_eq 0 below · cited by 8 · depth 18
• Triviality of an idele class character with trivial local components NumberField.TateGlobal.eq_one_of_isIdeleClassChar_of_continuous_of_forall_localChar_eq_one 2 below · cited by 6 · depth 19
• Integrability of tempered idele functions against ‖·‖^σ NumberField.TateGlobal.exists_forall_integrable_norm_mul_ideleNorm_rpow_of_valuation_of_prod_norm_pow_mul_le 10 below · cited by 3 · depth 19
• Conductor exponent of an idele character under adelic base change NumberField.TateGlobal.exists_hasConductorExponentAt_localChar_comp_genuineBeta_le 0 below · cited by 1 · depth 19
• Idele norm of a determinant embedded at one finite place NumberField.TateGlobal.ideleNorm_det_placeEmbed 5 below · cited by 10 · depth 19
• Unramifiedness of μ∘ N_{M/E} at an unramified prime NumberField.TateGlobal.isUnramifiedCharAt_comp_idelicNorm_genuineBaseChange_iff_of_ramificationIdx_eq_one 6 below · cited by 4 · depth 19
• Restriction of an idele class character to a subfield NumberField.TateGlobal.exists_isIdeleClassChar_continuous_localChar_eq_finprod_localChar_extension_algebraMap 0 below · cited by 2 · depth 20
• Meromorphic continuation of a partial Hecke Euler product NumberField.TateGlobal.exists_meromorphicOn_eq_partialEulerProduct 50 below · cited by 3 · depth 20
• Unramified local characters above an unramified prime NumberField.TateGlobal.finprod_localChar_extension_algebraMap_eq_finprod_apply_uniformizerIdele_zpow_of_ramificationIdx_eq_one_of_isUnramifiedCharAt 0 below · cited by 2 · depth 20
• Local components at -1 of a norm-composite idele character NumberField.TateGlobal.finprod_mem_primeFibre_localChar_comp_idelicNorm_apply_neg_one 0 below · cited by 1 · depth 20
• Parity of an idele class character of ℚ at -1 NumberField.TateGlobal.prod_localChar_apply_neg_one_eq_neg_one_zpow_of_isArchCompAt 0 below · cited by 3 · depth 20
• Holomorphy at s=1 of a nontrivial Hecke L-function NumberField.TateGlobal.exists_meromorphicOn_analyticAt_one_eq_partialEulerProduct_of_ne_one 50 below · cited by 2 · depth 21
• Idele class characters of ℚ: local component at v is 1 on -1 NumberField.TateGlobal.localChar_apply_neg_one_eq_one_of_isIdeleClassChar_of_isArchCompAt_zero_zero 0 below · cited by 6 · depth 21
• Meromorphic continuation and functional equation of Tate's zeta integral NumberField.TateGlobal.zetaIntegral_meromorphic_continuation_fe 45 below · cited by 1 · depth 21
• Tate's global zeta integral: holomorphy at s=1 for χ≠ 1 NumberField.TateGlobal.zetaIntegral_meromorphic_continuation_fe_analyticAt_one_of_ne_one 45 below · cited by 1 · depth 22
• Partial Hecke L-function of a nontrivial unitary idele class character on Re w>0 NumberField.TateGlobal.exists_forall_differentiableOn_eq_sub_mul_partialEulerProduct_localChar_of_ne_one 61 below · cited by 1 · depth 23
• Idele factorisation: principal times balanced dilation times compact NumberField.TateGlobal.exists_isCompact_forall_eq_principal_mul_balanced_mul 6 below · cited by 2 · depth 23
• Volume of a norm slab of idele classes NumberField.TateGlobal.exists_measure_fundamentalDomain_inter_ideleNorm_Icc_eq_mul_log 6 below · cited by 8 · depth 23
• Compact subgroups of GL₂(A_F) have determinants of idelic norm 1 NumberField.TateGlobal.ideleNorm_det_eq_one_of_isCompact_of_mem 2 below · cited by 9 · depth 23
• Fujisaki compactness: compact representatives for norm-one ideles NumberField.TateGlobal.exists_isCompact_subset_normOneIdeles_forall_mem_exists_eq_map_algebraMap_mul 3 below · cited by 34 · depth 24
• A Haar measure and fundamental domain with finite positive shell mass NumberField.TateGlobal.exists_isHaarMeasure_isFundamentalDomain_measure_inter_shell_ne_zero_ne_top 12 below · cited by 4 · depth 24
• Borel fundamental domain for the principal ideles NumberField.TateGlobal.exists_measurableSet_forall_isFundamentalDomain_range_unitsMap_algebraMap 3 below · cited by 8 · depth 25
• Fibre integration of the idele norm over a fundamental domain NumberField.TateGlobal.exists_setIntegral_comp_ideleNorm_eq_mul_integral_Ioi_and_setIntegral_ideleNorm_cpow_eq_div 51 below · cited by 12 · depth 25
• Tate's main theorem: entire part plus polar part NumberField.TateGlobal.exists_setIntegral_eq_entirePart_add_polarPart_and_fe_of_thetaInversion 54 below · cited by 4 · depth 25
• Tate's truncated zeta integral under theta inversion NumberField.TateGlobal.setIntegral_eq_upperHalves_add_poleIntegrals_of_thetaInversion 53 below · cited by 1 · depth 26
• Vanishing of int_Ω χ(a)g(‖a‖) dν for χ nontrivial on norm-one ideles NumberField.TateGlobal.setIntegral_mul_apply_ideleNorm_eq_zero_of_isIdeleClassChar_of_exists_ideleNorm_eq_one_ne 3 below · cited by 6 · depth 26
• Logarithmic measure of idele norm slabs in a fundamental domain NumberField.TateGlobal.exists_pos_forall_measure_inter_setOf_ideleNorm_mem_Icc_eq_ofReal_mul_log 52 below · cited by 4 · depth 27
• Idelic norms of determinants on GL₂(A_ℚ) NumberField.TateGlobal.ideleNorm_det_facts_rankinSelberg_rat 7 below · cited by 1 · depth 27
• Idelic norm of a base-changed idele NumberField.TateGlobal.ideleNorm_idelesBaseChange 1 below · cited by 10 · depth 27
• Non-vanishing of partial Hecke L-functions on Re w ≥ 1 NumberField.TateGlobal.exists_analyticOnNhd_mul_partialEulerProduct_eq_one_of_isUnitaryChar_of_isIdeleClassChar 71 below · cited by 2 · depth 28
• Archimedean parameters and weights of a unitary idelic character NumberField.TateGlobal.exists_archParam_weight_archLocalChar_eq_of_isUnitaryChar 6 below · cited by 14 · depth 28
• Entire continuation of Hecke L-functions with explicit Γ-factors NumberField.TateGlobal.exists_differentiable_eq_eulerProduct_and_eq_prod_Gamma_mul_of_archLocalChar_eq 90 below · cited by 4 · depth 28
• Factorisable adelic integrals as products of local zeta values NumberField.TateGlobal.exists_forall_integral_eq_mul_prod_localZeta_of_eq_indicator 3 below · cited by 1 · depth 28
• Hecke–Tate functional equation with pinned local data NumberField.TateGlobal.exists_forall_prod_Gamma_mul_eulerProduct_one_sub_eq_mul_cpow_mul_of_archLocalChar_eq 109 below · cited by 1 · depth 28
• Uniform zero-free region and L'/L bounds for Hecke L-functions NumberField.TateGlobal.exists_zeroFree_norm_deriv_le_and_inv_le_eulerProduct_continuation_of_archLocalChar_eq 146 below · cited by 2 · depth 28
• Entire L and Λ for non-norm-power idele class characters NumberField.TateGlobal.exists_differentiable_eq_eulerProduct_and_eq_prod_Gamma_mul_of_archLocalChar_eq_of_ne_normPowChar 82 below · cited by 1 · depth 29
• Entire continuation of the completed zeta for norm-power characters NumberField.TateGlobal.exists_differentiable_eq_sub_mul_eulerProduct_and_eq_mul_prod_Gamma_mul_of_eq_normPowChar 10 below · cited by 1 · depth 29
• Entire zeta integral and functional equation for Hecke characters NumberField.TateGlobal.exists_entire_zetaIntegral_eq_mul_prod_Gamma_mul_eulerProduct_and_one_sub_eq_root_mul_cpow_of_archLocalChar_eq 108 below · cited by 2 · depth 29
• Convexity bound for partial Hecke L-functions in a strip NumberField.TateGlobal.exists_forall_norm_partialEulerProduct_continuation_le_rpow_of_re_mem_Icc_of_admitsModulus 104 below · cited by 2 · depth 29
• Convexity bound for (s-1)ζ_{K,T} in a vertical strip NumberField.TateGlobal.exists_forall_norm_sub_one_mul_partialDedekindZeta_continuation_le_rpow_of_re_mem_Icc 8 below · cited by 3 · depth 29
• De la Vallée Poussin zero-free region for partial Hecke L-functions NumberField.TateGlobal.exists_pos_forall_partialEulerProduct_continuation_ne_zero_of_one_sub_div_log_le_re_of_admitsModulus 142 below · cited by 1 · depth 29
• De la Vallée Poussin zero-free region for ζ_{K,T} NumberField.TateGlobal.exists_pos_forall_sub_one_mul_partialDedekindZeta_continuation_ne_zero_of_one_sub_div_log_le_re 13 below · cited by 1 · depth 29
• Unramified χ∘det on Hecke words over GL₂(Kᵥ) NumberField.TateGlobal.sum_localChar_det_heckeWord_eq_pow_mul_pow_of_isUnramifiedCharAt 0 below · cited by 1 · depth 29
• Uniform finiteness bound for unramified idele class characters NumberField.TateGlobal.exists_forall_finite_and_card_le_of_archLocalChar_eq_cpow_const_of_pairwise_ne_normOneIdeles 9 below · cited by 1 · depth 30
• Polynomial bound on Re s=-1/2 for partial Hecke L-functions NumberField.TateGlobal.exists_forall_norm_partialEulerProduct_continuation_le_rpow_on_re_eq_neg_half_of_admitsModulus 99 below · cited by 1 · depth 30
• Euler product of the global Tate zeta integral (S-form) NumberField.TateGlobal.exists_forall_zetaIntegral_mul_eulerFactors_eq_of_eq_indicator 0 below · cited by 1 · depth 30
• Unit relation for archimedean parameters of unramified idele class characters NumberField.TateGlobal.exists_int_sum_mult_mul_mul_log_eq_two_pi_mul_of_isIdeleClassChar_of_archLocalChar_eq_cpow 5 below · cited by 1 · depth 30
• Vertical-strip Gaussian bound for a partial Hecke L-function NumberField.TateGlobal.exists_norm_partialEulerProduct_continuation_le_mul_exp_mul_im_sq 95 below · cited by 1 · depth 30
• Zero-free disc at s=1-iθ/2 for self-dual Hecke characters NumberField.TateGlobal.exists_pos_forall_partialEulerProduct_continuation_ne_zero_of_norm_sub_le_of_sq_eq_normPowChar_of_admitsModulus 76 below · cited by 1 · depth 30
• Tate: covolume rate of K^× in the ideles NumberField.TateGlobal.measure_fundamentalDomain_inter_ideleNorm_Icc_eq_measure_unitShell_mul_classNumber_mul_regulator_div 13 below · cited by 1 · depth 30
• Everywhere-unramified idele characters kill integral unit ideles NumberField.TateGlobal.eq_one_of_forall_isUnramifiedCharAt_of_fst_eq_one_of_mem_adicCompletionIntegers 0 below · cited by 1 · depth 31
• Index of K^×·(K_∞^××widehat𝒪^×) is h_K NumberField.TateGlobal.index_unitIdelesOutside_sup_range_unitsMap_algebraMap_eq_classNumber 1 below · cited by 1 · depth 31
• Regulator term for unit idele classes of bounded norm NumberField.TateGlobal.measure_unitIdeles_inter_fundamentalDomain_inter_ideleNorm_Icc_eq_measure_unitShell_mul_regulator_div 10 below · cited by 1 · depth 31
• Euler product, S-correction and partial product multiply to one NumberField.TateGlobal.differentiable_and_eulerProduct_mul_prod_mul_partialEulerProduct_eq_one_and_prod_ne_zero 3 below · cited by 1 · depth 32
• Uniqueness of the archimedean parameter at an infinite place NumberField.TateGlobal.eq_of_archLocalChar_eq_ideleNorm_cpow_of_archLocalChar_eq_ideleNorm_cpow 4 below · cited by 1 · depth 32
• Idele norm of the S-part of a principal idele NumberField.TateGlobal.ideleNorm_partAt_algebraMap_eq_prod_norm_pow_mult_mul_prod_norm 8 below · cited by 3 · depth 32
• Product formula for a principal idele split along S and T NumberField.TateGlobal.ideleNorm_partAt_mul_prod_norm_mul_finprod_norm_eq_one 5 below · cited by 3 · depth 32
• Quotient μν⁻¹ of unitary idele class characters NumberField.TateGlobal.isUnitaryChar_isIdeleClassChar_localChar_archLocalChar_mul_inv 0 below · cited by 1 · depth 32
• Twisting a unitary idele class character by ‖·‖^{it₀} NumberField.TateGlobal.isUnitaryChar_isIdeleClassChar_localChar_archLocalChar_mul_normPowChar 12 below · cited by 2 · depth 32
• Idele norm one for an archimedean unit of modulus one NumberField.TateGlobal.ideleNorm_archUnitHom_eq_one_of_norm_extensionEmbedding_eq_one 4 below · cited by 1 · depth 33
• Unramified local character agrees at any uniformizer NumberField.TateGlobal.localChar_apply_eq_apply_uniformizerIdele_of_isUnramifiedCharAt 0 below · cited by 1 · depth 33
• Polynomial lower bound for a partial Hecke L-function on Re w≥ 1 NumberField.TateGlobal.exists_forall_one_le_mul_norm_apply_of_differentiable_of_eq_partialEulerProduct 100 below · cited by 2 · depth 36
• Polynomial lower bound for regularised shifted partial Dedekind zeta NumberField.TateGlobal.exists_one_le_mul_norm_of_eq_sub_mul_partialEulerProduct_normPowChar 78 below · cited by 2 · depth 36
• Polynomial growth of partial Hecke L-functions on vertical strips NumberField.TateGlobal.exists_forall_norm_le_mul_of_differentiable_of_eq_partialEulerProduct_of_re_mem_Icc 77 below · cited by 2 · depth 37
• Polynomial vertical-strip bound for a regularised partial zeta function NumberField.TateGlobal.exists_forall_norm_le_mul_of_eq_sub_mul_partialEulerProduct_normPowChar_of_re_mem_Icc 8 below · cited by 3 · depth 37
• Non-vanishing of partial Hecke L-functions on Re s=1 NumberField.TateGlobal.exists_tendsto_punctured_ne_zero_of_eq_partialEulerProduct 71 below · cited by 2 · depth 37
• Bounded entire continuation of a unitary idele class L-function NumberField.TateGlobal.exists_differentiable_forall_norm_le_and_eq_mul_prod_GammaReal_mul_tprod_of_isUnitaryChar 74 below · cited by 1 · depth 38
• Unramified twists normalising pairs of unitary Hecke characters NumberField.TateGlobal.exists_finite_forall_exists_isUnramifiedCharAt_mul_mul_pow_two_mem_abs_archParam_le_of_localChar_eq 62 below · cited by 1 · depth 40
• Unramified unitary Hecke characters of nearly prescribed archimedean type NumberField.TateGlobal.exists_forall_exists_isIdeleClassChar_isUnramifiedCharAt_archLocalChar_eq_abs_sub_le 4 below · cited by 1 · depth 41

NumberField.Units 2

• Dirichlet's unit theorem as a covering of the trace-zero hyperplane NumberField.Units.exists_forall_abs_sub_mult_mul_log_le 0 below · cited by 2 · depth 18
• Units balance positive weights at all infinite places NumberField.Units.exists_forall_abs_two_mul_log_add_log_sub_div_le 0 below · cited by 1 · depth 32

NumberField.mixedEmbedding 27

• Polynomial decay in t of dilated archimedean lattice sums over a fractional ideal NumberField.mixedEmbedding.exists_forall_tsum_fractionalIdeal_weight_le_rpow_neg 0 below · cited by 11 · depth 16
• Trace dual of the Minkowski lattice of a fractional ideal NumberField.mixedEmbedding.coe_dualSubmodule_flip_traceForm_idealLattice 2 below · cited by 3 · depth 17
• Nondegeneracy of the trace form on the mixed space NumberField.mixedEmbedding.traceForm_mixedSpace_nondegenerate 1 below · cited by 9 · depth 17
• Uniform integral approximation at all infinite places NumberField.mixedEmbedding.exists_forall_norm_embedding_sub_le 0 below · cited by 1 · depth 18
• Trace on the mixed space extends the field trace NumberField.mixedEmbedding.trace_mixedEmbedding 0 below · cited by 8 · depth 18
• Trace of the mixed space of a number field over ℝ NumberField.mixedEmbedding.trace_mixedSpace_apply 0 below · cited by 2 · depth 19
• Summability of a translated Schwartz sum over 𝒪_F NumberField.mixedEmbedding.summable_norm_schwartzMap_ringOfIntegers_translate 0 below · cited by 1 · depth 24
• Dilation form of lattice decay for Fourier transforms on the mixed space NumberField.mixedEmbedding.exists_bound_tsum_norm_vectorFourierIntegral_comp_mul_inv 5 below · cited by 2 · depth 26
• Uniform lattice-sum decay for Fourier transforms on the mixed space NumberField.mixedEmbedding.exists_bound_tsum_norm_vectorFourierIntegral_mul_ringOfIntegers 4 below · cited by 1 · depth 27
• Uniform decay bound for sheared two-variable lattice sums over a number field NumberField.mixedEmbedding.exists_sum_inv_one_add_norm_mul_pow_mul_inv_one_add_norm_add_mul_pow_le 0 below · cited by 1 · depth 27
• Uniform bound for Schwartz sums over nonzero integers NumberField.mixedEmbedding.exists_bound_tsum_norm_schwartzMap_mul_ringOfIntegers 0 below · cited by 1 · depth 28
• Sheared two-variable lattice sum bound over ℚ NumberField.mixedEmbedding.exists_sum_inv_one_add_norm_pow_mul_inv_one_add_norm_add_mul_pow_le_mul_one_add_inv_rat 0 below · cited by 1 · depth 29
• Uniform lower bound for place-weighted products of ideal-lattice forms NumberField.mixedEmbedding.exists_pos_forall_le_prod_placeNorm_pow_mult_sum_mul_repr_stdBasis 0 below · cited by 1 · depth 31
• Absolute algebra norm on the mixed space equals `mixedEmbedding.norm` NumberField.mixedEmbedding.abs_algebraNorm_eq_norm 0 below · cited by 1 · depth 32
• Smooth exponential–polar coordinates on mixed-space units NumberField.mixedEmbedding.exists_contDiff_periodic_normAtPlace_eq_exp_div_mult_polarCoord_units 0 below · cited by 4 · depth 32
• Norm slabs of the fundamental cone: int dV/N = vol(N≤ 1)log(b/a) NumberField.mixedEmbedding.fundamentalCone.setLIntegral_inv_norm_eq_volume_normLeOne_mul_log 0 below · cited by 1 · depth 32
• Mass of the archimedean unit shell for dx/N(x) NumberField.mixedEmbedding.setLIntegral_setOf_forall_normAtPlace_mem_Icc_one_exp_inv_norm_eq_two_pow_mul_two_pi_pow 0 below · cited by 1 · depth 32
• Unitary invariance of the matrix Laplacian over the mixed space NumberField.mixedEmbedding.sum_iteratedFDeriv_two_comp_conj_eq_of_mul_conjTranspose_eq_one 0 below · cited by 1 · depth 32
• Circle character on a unit lattice from complex arguments and tilt phases NumberField.mixedEmbedding.exists_addMonoidHom_addCircle_lift_arg_of_injOn 0 below · cited by 2 · depth 33
• Smooth periodic box-supported window in log-moduli and angle slots NumberField.mixedEmbedding.exists_contDiff_periodic_forall_apply_eq_prod_zpow_neg_mul_apply_mul_of_polarCoord 0 below · cited by 3 · depth 33
• Gram measure of the trace form on K_∞ equals 2^{r₂} times Lebesgue measure NumberField.mixedEmbedding.gram_trace_smul_map_volume_eq_two_pow_nrComplexPlaces_smul_volume 1 below · cited by 1 · depth 33
• Totally positive units have trivial sign in polar coordinates NumberField.mixedEmbedding.sgn_eq_one_of_forall_pos_of_polarCoord 0 below · cited by 2 · depth 33
• Smoothness and support under inversion and the twist (a,b)↦(a,ba⁻¹) NumberField.mixedEmbedding.contDiff_comp_ringInverse_and_contDiff_mul_twist_of_tsupport_subset_units 0 below · cited by 2 · depth 35
• Exponential–polar coordinates on the mixed space NumberField.mixedEmbedding.exists_contDiff_periodic_normAtPlace_eq_exp_polarCoord_units_and_fst_eq_and_snd_eq 0 below · cited by 1 · depth 35
• Kink-basis windows from exponential–polar coordinates NumberField.mixedEmbedding.exists_kinkWindows_forall_add_sum_abs_one_sub_exp_mul_add_sum_norm_one_sub_cexp_sq_mul_log_mul_eq_prod_zpow_neg_mul_of_polarCoord 1 below · cited by 1 · depth 35
• Splitting off a complex coordinate of the mixed space NumberField.mixedEmbedding.exists_continuousLinearEquiv_measurePreserving_fst_eq_of_isComplex 0 below · cited by 2 · depth 37
• Splitting off a real coordinate of the mixed space, measure preservingly NumberField.mixedEmbedding.exists_continuousLinearEquiv_measurePreserving_fst_eq_of_isReal 0 below · cited by 1 · depth 37