← all areas

Namespace AlgebraicClosure 11 theorems

• Open subgroup containing all inertia is all of G_ℚ AlgebraicClosure.subgroup_eq_top_of_inertiaSubgroupIn_le 3 below · cited by 5 · depth 7
• Open subgroups containing all inertia-with-ζ₃ contain Gal(ℚ̄/ℚ(ζ₃)) AlgebraicClosure.stabilizer_primitiveRoot_three_le_of_isOpen_of_forall_inertia_inf_le 4 below · cited by 1 · depth 8
• Existence of a mod q cyclotomic character family AlgebraicClosure.exists_cycloChar_family 0 below · cited by 4 · depth 10
• Uniform finite level for characters unramified outside S AlgebraicClosure.exists_uniform_level_of_characters_unramified_outside 2 below · cited by 3 · depth 10
• Automorphisms of ℚ̄ act on n-th roots of unity by a power AlgebraicClosure.exists_apply_eq_pow_of_pow_eq_one 0 below · cited by 7 · depth 14
• Characters of G_ℚ unramified everywhere are trivial AlgebraicClosure.monoidHom_eq_one_of_inertiaSubgroupIn_le_ker 4 below · cited by 1 · depth 15
• Cyclotomic character is trivial mod pⁿ on a finite level AlgebraicClosure.exists_intermediateField_toZModPow_cyclotomicCharacter_eq_one 0 below · cited by 1 · depth 18
• Mod-L cyclotomic character takes value ℓ at Frobenius AlgebraicClosure.exists_monoidHom_zmod_units_frobenius_eq_unitOfCoprime 2 below · cited by 1 · depth 18
• Automorphisms of mathbb Qₚ̄ descend along ℚ̄hookrightarrowmathbb Qₚ̄ AlgebraicClosure.exists_ratAlgEquiv_of_padicAlgEquiv_comp 0 below · cited by 1 · depth 18
• Galois descent of linear independence over ℚ̄ AlgebraicClosure.linearIndependent_of_linearIndependent_rat_of_forall_apply_smul 0 below · cited by 1 · depth 18
• Embedding ℚ̄ into mathbb Qₚ̄ over ℚ AlgebraicClosure.nonempty_algHom_rat_padicAlgClosure 0 below · cited by 1 · depth 18