← all areas

Namespace IsPrimitiveRoot 11 theorems

• Discrete logarithm on μₚ: unique ℤ/p-valued exponents IsPrimitiveRoot.existsUnique_eq_pow_val 0 below · cited by 4 · depth 16
• Lifting ζ_q to ζ_{qℓ} over a henselian base IsPrimitiveRoot.exists_isPrimitiveRoot_mul_pow_eq_and_mem_and_ringHom_apply_eq_exp_of_henselian 0 below · cited by 1 · depth 29
• Adjoining a primitive q-th root of unity to a complete DVR IsPrimitiveRoot.exists_isDiscreteValuationRing_isAdicComplete_ringHom_comp_eq_maximalIdeal_eq_span_pow_sub_one_eq_mul_of_adjoin_eq_top 2 below · cited by 3 · depth 32
• Totally ramified q-cyclotomic extension of a DVR with 𝔪=(q) IsPrimitiveRoot.exists_algHom_apply_eq_of_geom_sum_eq_zero_and_eq_mul_one_sub_and_pow_sub_one_eq_mul_of_adjoin_eq_top 0 below · cited by 1 · depth 33
• Cyclotomic ramification over a complete coefficient ring, all primes IsPrimitiveRoot.exists_isDiscreteValuationRing_isAdicComplete_ringHom_comp_eq_maximalIdeal_eq_span_pow_sub_one_eq_mul_of_adjoin_eq_top_of_prime 3 below · cited by 2 · depth 33
• 1-ζ is a uniformiser when v(q)=q-1 IsPrimitiveRoot.exists_isUnit_one_sub_eq_mul_of_pow_sub_one_eq_mul 0 below · cited by 6 · depth 33
• Embedding a cyclotomic extension of ℚ sending ζₙ to a given root IsPrimitiveRoot.exists_ringHom_zeta_eq_of_isCyclotomicExtension 0 below · cited by 11 · depth 33
• Cyclotomic discrete valuation ring mapping to a local domain IsPrimitiveRoot.exists_isDiscreteValuationRing_ringHom_pow_sub_one_eq_mul_of_charP_residueField 0 below · cited by 1 · depth 34
• Ideals (b-ω^k) are generated by idempotents IsPrimitiveRoot.exists_isIdempotentElem_span_sub_pow_eq 0 below · cited by 2 · depth 34
• Branches of A ⊗_{Z_0} C at a root of Φ_q IsPrimitiveRoot.exists_tmul_sub_tmul_mem_of_aeval_cyclotomic_eq_zero 0 below · cited by 4 · depth 34
• Cyclotomic discrete valuation ring below a primitive q-th root of unity IsPrimitiveRoot.exists_isDiscreteValuationRing_ringHom_pow_sub_one_eq_mul_of_charP_residueField_of_prime 0 below · cited by 1 · depth 35