← all areas

Namespace FrobeniusDensity 23 theorems

• Frobenius's density theorem, qualitative form FrobeniusDensity.statement 15 below · cited by 34 · depth 8
• Degree-one prime sums for fixed fields of Gal(L/ℚ) FrobeniusDensity.degOneAsymptotic 6 below · cited by 2 · depth 9
• Frobenius elements in Gal(ℚ̄/ℚ) from the density statement FrobeniusDensity.exists_frobenius_conj_pow_of_statement 3 below · cited by 8 · depth 9
• Frobenius density from the degree-one prime asymptotic FrobeniusDensity.statement_of_degOneAsymptotic 7 below · cited by 1 · depth 9
• Degree-one prime sum plus log(s-1) is bounded FrobeniusDensity.degOneSum_add_log_isBigO 4 below · cited by 2 · depth 10
• Involutions in G_ℚ are Frobenius conjugates on finite levels FrobeniusDensity.exists_frobenius_conj_of_mul_self_eq_one_of_statement 3 below · cited by 1 · depth 10
• Frobenius-power density for subgroups containing Gal(ℚ̄/F) FrobeniusDensity.frobeniusPowerDense_of_le_ker 20 below · cited by 9 · depth 10
• Nonzero conjugating count iff some power of σ is conjugate to τ FrobeniusDensity.ncard_conj_gen_ne_zero_iff 0 below · cited by 1 · depth 10
• Degree-one primes over ℓ count Frobenius-fixed cosets of G/H FrobeniusDensity.ncard_degreeOne_primesOver_eq_ncard_frobFixed 2 below · cited by 2 · depth 10
• Positivity of sum_{f∣ n}μ(n/f)f for n the order of a group element FrobeniusDensity.sum_moebius_mul_pos 1 below · cited by 1 · depth 10
• Summability of the degree-one prime series for s>1 FrobeniusDensity.summable_degOne_term 2 below · cited by 1 · depth 10
• Möbius-weighted fixed-coset count equals count of conjugating elements FrobeniusDensity.weight_eq 1 below · cited by 2 · depth 10
• Chebotarev existence: every element is conjugate to a Frobenius FrobeniusDensity.exists_isFrobeniusAt_conj_mem_of_le_ker 16 below · cited by 18 · depth 11
• Finiteness of the ideal sum sum_I (NI)^{-s} for s>1 FrobeniusDensity.idealSum_ne_top 0 below · cited by 4 · depth 11
• Degree-one primes over ℓ count cosets fixed by D_{Q_0} FrobeniusDensity.ncard_degreeOne_primesOver_under 1 below · cited by 1 · depth 11
• Splitting the prime-ideal Dirichlet sum into degree-one, cut and tail parts FrobeniusDensity.primeSum_eq_degOneSum_add 0 below · cited by 2 · depth 11
• Prime ideal sum is log1s-1+O(1) as s→1⁺ FrobeniusDensity.primeSum_toReal_add_log_isBigO 2 below · cited by 4 · depth 11
• Decomposition group generated by Frobenius at an unramified prime FrobeniusDensity.stabilizer_eq_zpowers_arithFrobAt 0 below · cited by 4 · depth 11
• Residue at s=1 of the ideal-norm sum for K FrobeniusDensity.tendsto_sub_one_mul_idealSum_test 1 below · cited by 1 · depth 12
• Primes of residue degree ≥ 2: a tail bound FrobeniusDensity.tailSum_le 0 below · cited by 4 · depth 15
• Conjugacy class size times centralizer order equals |G| FrobeniusDensity.card_setOf_isConj_mul_card_centralizer 0 below · cited by 1 · depth 17
• Class count for an order-8 element conjugate to its cube FrobeniusDensity.ncard_conj_gen_eq_of_orderOf_eq_eight 0 below · cited by 1 · depth 17
• Möbius inversion of Gauss's totient identity FrobeniusDensity.sum_moebius_mul_eq_totient 0 below · cited by 1 · depth 17