← all areas

Namespace ValuationSubring 337 theorems

— 332 · IsFrobeniusAt 5

directly in ValuationSubring 332

• Existence of a Frobenius element at a place above q ValuationSubring.exists_isFrobeniusAt_of_liesOverPrime 1 below · cited by 51 · depth 6
• Existence of a place of ℚ̄ above ℓ with Frobenius ValuationSubring.exists_isFrobeniusAt_rat 2 below · cited by 40 · depth 6
• Decomposition group elements preserve the valuation of ℚ̄ ValuationSubring.valuation_map_eq_of_mem_decompositionSubgroup 0 below · cited by 25 · depth 6
• Every place of ℚ̄ above q localises ℤ̄ ValuationSubring.exists_integral_mul_eq_of_liesOverPrime 0 below · cited by 6 · depth 7
• Mod p cyclotomic character surjects onto inertia at p ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_pow 0 below · cited by 30 · depth 7
• The residue field of a valuation subring of an algebraically closed field ValuationSubring.isAlgClosed_residueField 1 below · cited by 200 · depth 7
• Integers prime to q are units at a valuation of residue characteristic q ValuationSubring.valuation_natCast_eq_one_of_not_dvd 0 below · cited by 9 · depth 7
• Inertia at q fixes roots of unity of order prime to q ValuationSubring.apply_eq_self_of_pow_eq_one_of_mem_inertiaSubgroupIn 0 below · cited by 15 · depth 8
• Frobenius conjugation raises tame inertia to the q-th power ValuationSubring.exists_algEquiv_conj_mul_pow_inv_wild_of_liesOverPrime 2 below · cited by 5 · depth 8
• Galois transitivity on the places of ℚ̄ above q ValuationSubring.exists_algEquiv_smul_eq_of_liesOverPrime 1 below · cited by 29 · depth 8
• Existence of a place above p with a Frobenius element ValuationSubring.exists_liesOverPrime_isFrobeniusAt_ratAlgClosure 4 below · cited by 29 · depth 8
• Inertial automorphism lies in inertia of a place above q ValuationSubring.exists_liesOverPrime_mem_inertiaSubgroupIn 0 below · cited by 9 · depth 8
• Monic polynomials over a valuation subring of an algebraically closed field have roots in it ValuationSubring.exists_root_mem_of_monic 0 below · cited by 2 · depth 8
• Rational numbers in a valuation subring above q ValuationSubring.ratCast_mem_iff_padicValRat_nonneg 4 below · cited by 36 · depth 8
• Equal residues iff valuation of difference is <1 ValuationSubring.residue_eq_residue_iff_valuation_sub_lt_one 0 below · cited by 3 · depth 8
• Nonzero residue iff valuation one in a valuation subring ValuationSubring.residue_ne_zero_iff_valuation_eq_one 0 below · cited by 2 · depth 8
• Integers prime to q are units at a place over q ValuationSubring.valuation_intCast_eq_one_of_not_dvd 1 below · cited by 3 · depth 8
• Valuation of an integer in terms of v_A(q) ValuationSubring.valuation_intCast_eq_pow_padicValInt 2 below · cited by 3 · depth 8
• Multiples of q have valuation <1 ValuationSubring.valuation_intCast_lt_one_of_dvd 0 below · cited by 1 · depth 8
• Inertia elements fix valuation ring elements modulo the maximal ideal ValuationSubring.valuation_sub_lt_one_of_mem_inertiaSubgroupIn 0 below · cited by 16 · depth 8
• Inertia subgroups restrict along finite normal subextensions of ℚ̄ ValuationSubring.exists_inertiaSubgroup_restrictNormal_eq 0 below · cited by 2 · depth 9
• Existence of a Frobenius element at a place of ℚ̄ above p ValuationSubring.exists_isFrobeniusAt_of_liesOverPrime_algebraicClosure_rat 2 below · cited by 17 · depth 9
• Existence of a place of ℚ̄ above each prime p ValuationSubring.exists_liesOverPrime_algebraicClosure_rat 0 below · cited by 95 · depth 9
• Inertia above an odd prime negates a square root of p ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_neg_of_sq_eq_prime 7 below · cited by 1 · depth 9
• Tame character attains a primitive m-th root of unity on inertia ValuationSubring.exists_mem_inertiaSubgroupIn_isPrimitiveRoot_tameCharacter 11 below · cited by 14 · depth 9
• Residue fields of valuation rings of ℚ̄ are algebraically closed ValuationSubring.isAlgClosed_residueField_algebraicClosure_rat 0 below · cited by 197 · depth 9
• A place of ℚ̄ restricts to a DVR on a number field ValuationSubring.isDiscreteValuationRing_comap_of_liesOverPrime 0 below · cited by 15 · depth 9
• Residue field of a valuation subring over ℓ has characteristic ℓ ValuationSubring.residueField_charP_of_liesOverPrime 0 below · cited by 70 · depth 9
• Valuation of an integer as an ℓ-th power ValuationSubring.valuation_intCast_eq_pow_pow_of_dvd 3 below · cited by 1 · depth 9
• Valuation of a rational in terms of v_q ValuationSubring.valuation_ratCast_eq_zpow_padicValRat 3 below · cited by 2 · depth 9
• Inertia subgroups conjugate under translation of valuation subrings ValuationSubring.conj_mem_inertiaSubgroupIn_of_mem_inertiaSubgroupIn_smul 1 below · cited by 24 · depth 10
• Inertia at q moves √[m]q by a primitive root ValuationSubring.exists_mem_inertiaSubgroupIn_primeLocalPlace_isPrimitiveRoot_apply_div 6 below · cited by 1 · depth 10
• Inertia acts by units with residue the tame character ValuationSubring.exists_units_mul_eq_and_residue_eq_tameCharacter_of_mem_inertiaSubgroupIn 2 below · cited by 5 · depth 10
• Localisation at a maximal ideal of ℤ̄ gives a Frobenius ValuationSubring.isFrobeniusAt_of_forall_smul_sub_pow_mem 0 below · cited by 4 · depth 10
• Valuation rings of algebraic extensions of ℚ have Krull dimension ≤ 1 ValuationSubring.krullDimLE_one_of_isAlgebraic_rat 2 below · cited by 7 · depth 10
• Cyclotomic character of Frobenius at ℓ ≠ p equals ℓ ValuationSubring.coe_cyclotomicCharacter_eq_natCast_of_isFrobeniusAt 0 below · cited by 6 · depth 11
• Mod-m cyclotomic character sends Frobenius at ℓ to ℓ ValuationSubring.cycloChar_eq_unitOfCoprime_of_isFrobeniusAt 1 below · cited by 17 · depth 11
• Inertia character factors through the p^k-quotient of (ℤ/q)^× ValuationSubring.exists_inertiaCharacter_eq_comp_of_forall_cyclotomic_eq_one 5 below · cited by 1 · depth 11
• Ramification of a Kummer extension witnessed by an inertia element ValuationSubring.exists_mem_inertiaSubgroupIn_fixing_ne_of_not_dvd_valuation 0 below · cited by 1 · depth 11
• Frobenius conjugation on inertia is a q-th power modulo pⁿ-th powers ValuationSubring.exists_mem_inertiaSubgroupIn_pow_eq_frobConj 2 below · cited by 7 · depth 11
• Tame inertia over q is cyclic modulo p^m-th powers ValuationSubring.exists_tame_generator_inertiaSubgroupIn 2 below · cited by 8 · depth 11
• Inertia character at q of exponent q-1 trivial when cyc(σ)=1 ValuationSubring.inertiaCharacter_eq_one_of_cyclotomic_eq_one 2 below · cited by 1 · depth 11
• Ring maps to characteristic ℓ kill the maximal ideal ValuationSubring.map_eq_zero_of_valuation_lt_one_of_charP 0 below · cited by 38 · depth 11
• Krull dimension of a valuation ring in characteristic zero ValuationSubring.ringKrullDim_le_toENat_trdeg_rat_add_one 1 below · cited by 2 · depth 11
• Inertia fixes roots of unity of order prime to q ValuationSubring.smul_eq_self_of_mem_inertiaSubgroupIn_of_pow_eq_one 0 below · cited by 17 · depth 11
• Independence of the tame character under unit change of π ValuationSubring.tameCharacter_eq_of_div_mem_of_div_mem 1 below · cited by 4 · depth 11
• Characters of a torsion monoid algebra land in the valuation subring ValuationSubring.addMonoidAlgebra_algHom_apply_mem_of_isOfFinAddOrder 0 below · cited by 6 · depth 12
• Trivial cyclotomic character on inertia fixes (q-1)-th roots of q ValuationSubring.apply_eq_self_of_pow_eq_prime_of_mem_inertiaSubgroupIn_of_cyc_eq_one 0 below · cited by 1 · depth 12
• Inertia-fixed discrete valuation subring at a place over ℓ ValuationSubring.exists_dvr_subring_mem_inertiaSubgroupIn_iff_forall_apply_eq 3 below · cited by 17 · depth 12
• DVR envelope at a place of ℚ̄ above ℓ ValuationSubring.exists_dvr_subring_of_forall_mem_decompositionSubgroup 4 below · cited by 5 · depth 12
• Wild elements act with q-power order at finite levels ValuationSubring.exists_forall_pow_prime_pow_apply_eq_self_of_wild 1 below · cited by 11 · depth 12
• Composite of a valuation ring with one of its residue field ValuationSubring.exists_le_forall_mem_iff_apply_mem 0 below · cited by 2 · depth 12
• Inertia at p realises every unit modulo p^k on p^k-th roots of unity ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_pow_of_pow_prime_pow_eq_one 0 below · cited by 17 · depth 12
• Inertia above 2 acts by ζ ↦ ζ³ on μ₄ ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_pow_three_of_pow_four_eq_one 0 below · cited by 6 · depth 12
• Inertia at the p-adic place comes from local inertia ValuationSubring.exists_mem_inertiaSubgroupIn_padicIntegers_localGaloisToGlobal_eq 2 below · cited by 6 · depth 12
• Inertia elements fixing all p-power roots of q are pⁿ-th powers ValuationSubring.exists_mem_inertiaSubgroupIn_pow_eq_of_forall_apply_eq 1 below · cited by 3 · depth 12
• Inertia at p moves μₚ for odd p ValuationSubring.exists_mem_inertiaSubgroup_cycloLift_ne_one 46 below · cited by 2 · depth 12
• Chevalley's extension theorem in place form ValuationSubring.exists_ringHom_extend_of_isAlgClosed 0 below · cited by 3 · depth 12
• Complete splitting forces trivial residue extension ValuationSubring.exists_sub_mem_nonunits_of_finrank_le_card 1 below · cited by 1 · depth 12
• Complete splitting forces trivial ramification in the value group ValuationSubring.exists_valuation_mul_eq_one_of_finrank_le_card 3 below · cited by 1 · depth 12
• Inertia characters of exponent n vanish on stabilisers of q^{1/n} ValuationSubring.inertiaCharacter_eq_one_of_apply_kummerRoot_eq 0 below · cited by 1 · depth 12
• Valuation rings of a function field in one variable are principal ValuationSubring.isPrincipalIdealRing_of_finiteDimensional_adjoin 0 below · cited by 36 · depth 12
• Inertia of a conjugate valuation subring ValuationSubring.mem_inertiaSubgroupIn_pointwise_smul_iff 0 below · cited by 4 · depth 12
• Reduction is bijective on m-th roots of unity ValuationSubring.residue_injOn_pow_eq_one_and_exists_residue_eq_of_isAlgClosed 0 below · cited by 7 · depth 12
• Abhyankar's inequality for Krull dimensions of valuation rings ValuationSubring.ringKrullDim_le_ringKrullDim_comap_add_trdeg 0 below · cited by 3 · depth 12
• Frobenius conjugation raises the tame character to the p-th power ValuationSubring.tameCharacter_conj_of_isFrobeniusAt 1 below · cited by 2 · depth 12
• Level-two tame character: its (p+1)-st power is cyclotomic ValuationSubring.tameCharacter_pow_succ_eq_natCast_of_pow_eq_of_mem_inertiaSubgroupIn 4 below · cited by 1 · depth 12
• Wild automorphisms fix points fixed by prime-to-q powers ValuationSubring.apply_eq_self_of_pow_apply_eq_self_of_wild 0 below · cited by 2 · depth 13
• p-adic decomposition subgroup lies in closure of local image ValuationSubring.decompositionSubgroup_padicPlace_le_closure_range_localGaloisToGlobal 1 below · cited by 7 · depth 13
• Regularity on both f-charts forces constancy ValuationSubring.exists_eq_algebraMap_of_forall_valuationSubring_mul_aeval_mem 0 below · cited by 3 · depth 13
• Residue-level approximation for incomparable valuation rings ValuationSubring.exists_forall_mem_and_sub_mem_nonunits 0 below · cited by 10 · depth 13
• Frobenius at a place restricts to arithmetic Frobenius ValuationSubring.exists_ideal_isArithFrobAt_restrictNormalHom_of_isFrobeniusAt 0 below · cited by 1 · depth 13
• Prime below a place of ℚ̄: inertia, wild part, uniformiser ValuationSubring.exists_ideal_ringOfIntegers_inertia_eq_map_restrictNormalHom 0 below · cited by 7 · depth 13
• Decomposition group surjects onto the stabiliser in a normal layer ValuationSubring.exists_mem_decompositionSubgroup_restrictNormal_eq 0 below · cited by 3 · depth 13
• Inertia at p surjects onto ℤₚ^× via χₚ ValuationSubring.exists_mem_inertiaSubgroupIn_cyclotomicCharacter_eq 1 below · cited by 11 · depth 13
• From L[f]-integrality to L[f⁻¹]-integrality after scaling ValuationSubring.exists_mul_pow_inv_mem_of_finiteDimensional_adjoin 0 below · cited by 5 · depth 13
• Kummer descent at a Galois-stable place ValuationSubring.exists_pow_eq_of_kummer_descent 0 below · cited by 2 · depth 13
• Residue field of a place of ℚ̄ above q is algebraic over mathbb F_q ValuationSubring.exists_pow_pow_eq_self_residueField_of_liesOverPrime 0 below · cited by 16 · depth 13
• Independent prolongation with enough residual witnesses has e=1 ValuationSubring.exists_valuation_mul_eq_one_of_forall_sup_eq_top 1 below · cited by 1 · depth 13
• Valuation subrings of algebraically closed fields are Henselian ValuationSubring.henselianLocalRing_of_isAlgClosed 0 below · cited by 54 · depth 13
• ℓ is irreducible in V∩ E when E is decomposition-fixed ValuationSubring.irreducible_natCast_comap_of_forall_smul_eq 2 below · cited by 1 · depth 13
• Local inertia maps into inertia at the p-adic place ValuationSubring.localGaloisToGlobal_mem_inertiaSubgroupIn_padicPlace 1 below · cited by 2 · depth 13
• Valuation criterion for membership in inertia ValuationSubring.mem_inertiaSubgroupIn_of_valuation_sub_lt_one 0 below · cited by 5 · depth 13
• Valuation subrings with prescribed trace on a subfield ValuationSubring.mem_of_forall_mem_iff_of_subset 0 below · cited by 1 · depth 13
• Residue 1 for p-power roots of unity above p ValuationSubring.residue_eq_one_of_pow_prime_pow_eq_one 0 below · cited by 3 · depth 13
• Ring maps to characteristic p kill the maximal ideal ValuationSubring.ringHom_apply_eq_zero_of_mem_maximalIdeal 0 below · cited by 7 · depth 13
• Multiplicativity of the tame character on inertia ValuationSubring.tameCharacter_mul_of_mem_inertiaSubgroupIn 1 below · cited by 15 · depth 13
• Tame character is multiplicative in powers of the uniformiser ValuationSubring.tameCharacter_pow_left 0 below · cited by 6 · depth 13
• The tame character of level two is killed by p²-1 ValuationSubring.tameCharacter_pow_sq_sub_one_eq_one_of_mem_inertiaSubgroupIn 0 below · cited by 7 · depth 13
• Tame character of ζ-1 equals the cyclotomic exponent ValuationSubring.tameCharacter_sub_one_eq_natCast 0 below · cited by 3 · depth 13
• Primitive factors in F ⊗_K A over a valuation subring ValuationSubring.tensorProduct_exists_primitive_factor 0 below · cited by 1 · depth 13
• Residue field of a place of ℚ̄ above ℓ has characteristic ℓ ValuationSubring.charP_residueField_of_liesOverPrime 0 below · cited by 27 · depth 14
• Valuation subrings of ℚ̄ over p have rank one ValuationSubring.eq_bot_of_isPrime_of_ne_maximalIdeal_of_liesOverPrime 1 below · cited by 24 · depth 14
• Decomposition of p(f)/t(f) with f^{-m}-tail and polynomial part ValuationSubring.exists_aeval_div_eq_aeval_div_add_inv_pow_mul_add_aeval_inv 1 below · cited by 1 · depth 14
• Inertia at q acts on qᶜ-th roots of unity ValuationSubring.exists_apply_eq_pow_and_apply_eq_self_of_mem_inertiaSubgroupIn_and_exists_mem_inertiaSubgroupIn_of_not_dvd 2 below · cited by 8 · depth 14
• Rank one: every nonzero element divides a power of a nonunit ValuationSubring.exists_dvd_pow_of_mem_maximalIdeal 0 below · cited by 21 · depth 14
• Zariski-local integrality of Gauss-ring coordinates of an integral element ValuationSubring.exists_eq_aeval_div_of_forall_valuationSubring_mem_of_eq_sum_mul 0 below · cited by 1 · depth 14
• Inertia-fixed elements factor as pⁿ times a unit ValuationSubring.exists_eq_prime_pow_mul_of_forall_mem_inertiaSubgroupIn_apply_eq 4 below · cited by 2 · depth 14
• Valuation subrings of K containing a Dedekind domain ValuationSubring.exists_eq_valuationSubringAtPrime_of_forall_algebraMap_mem 0 below · cited by 15 · depth 14
• Multivariate Hensel lemma over a valuation subring of an algebraically closed field ValuationSubring.exists_forall_eval_eq_zero_of_isUnit_det_jacobian 0 below · cited by 1 · depth 14
• Valuation subring of a number field with prescribed centre ValuationSubring.exists_heightOneSpectrum_asIdeal_eq_and_eq_valuationSubring_of_forall_mem_iff_valuation_lt_one 1 below · cited by 1 · depth 14
• Kummer decomposition of an additive equivariant inertia cocycle ValuationSubring.exists_kummer_decomposition_of_inertia_cocycle 8 below · cited by 1 · depth 14
• Local inertia approximates global inertia at finite level ValuationSubring.exists_localGaloisToGlobal_mem_inertiaSubgroupIn_inv_mul_mem_fixingSubgroup 3 below · cited by 1 · depth 14
• Denominator clearing over a valuation subring of L ValuationSubring.exists_polynomial_map_residue_ne_zero_eval_mul_mem 2 below · cited by 1 · depth 14
• ℤ_{(ℓ)} maps into every valuation subring over ℓ ValuationSubring.exists_ratLocalizedAt_ringHom_of_liesOverPrime 1 below · cited by 17 · depth 14
• Residue field of a valuation subring of an algebraically closed field ValuationSubring.isAlgClosed_residueField_of_isAlgClosed 0 below · cited by 124 · depth 14
• Restriction maps decomposition groups onto decomposition groups ValuationSubring.map_restrictNormalHom_decompositionSubgroup_eq 4 below · cited by 3 · depth 14
• Integral points as Galois-fixed points in a valuation ring ValuationSubring.natCard_algHom_int_eq_natCard_algHom_fixed_of_finite_of_liesOverPrime 1 below · cited by 1 · depth 14
• Residue field of a place of ℚ̄ above q ValuationSubring.nonempty_residueField_ringEquiv_algebraicClosure_zmod_of_liesOverPrime 1 below · cited by 16 · depth 14
• Frobenius constraint (χ₂(σ)²-1)sum nᵢ aᵢ = 0 on a decomposed corner ValuationSubring.sub_one_mul_sum_smul_eq_zero_of_corner_decomposition 19 below · cited by 1 · depth 14
• Gauss valuation ring contains Q(f) and its inverse ValuationSubring.aeval_mem_and_inv_mem_of_forall_mem_iff_of_mul_single_eq_ofPowerSeries 0 below · cited by 1 · depth 15
• A place of ℚ̄ above q meets ℚ in mathbb Z_{(q)} ValuationSubring.algebraMap_rat_mem_iff_of_liesOverPrime 0 below · cited by 3 · depth 15
• Valuation subrings of ℚ̄ over p come from absolute values ValuationSubring.exists_absoluteValue_isNonarchimedean_mem_iff_le_one_of_liesOverPrime 0 below · cited by 36 · depth 15
• Laurent decomposition of rational functions over a valuation ring ValuationSubring.exists_aeval_div_eq_aeval_div_add_aeval_inv_div 0 below · cited by 1 · depth 15
• Transitivity on valuation rings in an infinite Galois extension ValuationSubring.exists_algEquiv_forall_mem_iff_of_isGalois_infinite 3 below · cited by 4 · depth 15
• Inertia-fixed elements lie in a dominated DVR with uniformiser ℓ ValuationSubring.exists_dvr_subring_of_forall_mem_inertiaSubgroupIn 1 below · cited by 10 · depth 15
• Inertia-fixed elements of a place over ℓ are ℓ^s times a unit ValuationSubring.exists_eq_pow_mul_of_forall_mem_inertiaSubgroupIn 2 below · cited by 4 · depth 15
• Cyclotomically equivariant Kummer character has inertia-fixed radicand ValuationSubring.exists_inertia_fixed_kummer_generator_of_additive_character 7 below · cited by 1 · depth 15
• Gauss normalisation of a polynomial over a valuation subring ValuationSubring.exists_map_subtype_eq_C_inv_mul_and_map_residue_ne_zero 0 below · cited by 3 · depth 15
• Kummer independence of p from inertia-fixed units ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_mul_of_pow_eq_prime 17 below · cited by 1 · depth 15
• Tame inertia labels come from a character of 𝔽_{q²}^× ValuationSubring.exists_monoidHom_galoisField_units_forall_tameCharacter_eq_imp_eq_or_eq_pow 21 below · cited by 2 · depth 15
• Residue fields of valuation subrings of ℚ̄ are algebraic over 𝔽ₚ ValuationSubring.exists_pow_prime_pow_eq_self_of_isAlgebraic 0 below · cited by 3 · depth 15
• Gauss reduction of a q-expansion valuation ring ValuationSubring.exists_ringHom_laurentSeries_residueField_of_forall_mem_iff_exists_powerSeries 0 below · cited by 20 · depth 15
• Powers of v(π₀) eventually below any nonzero value ValuationSubring.exists_valuation_pow_lt_of_isAlgebraic 2 below · cited by 9 · depth 15
• Gauss valuations: residue degree bound and uniqueness at equality ValuationSubring.finrank_residueField_le_and_forall_mul_inv_mem_and_forall_eq_of_gauss 2 below · cited by 1 · depth 15
• Integers coprime to p are invertible in a valuation ring over p ValuationSubring.inv_natCast_mem_of_coprime_of_liesOverPrime 0 below · cited by 1 · depth 15
• Reduction into characteristic q has kernel mathfrak m_A ValuationSubring.ringHom_apply_eq_zero_iff_mem_maximalIdeal_of_charP 0 below · cited by 14 · depth 15
• Residue field of a valuation subring is algebraic over mathbb Fₚ ValuationSubring.algebra_isAlgebraic_zmod_residueField_of_isAlgebraic_rat 0 below · cited by 9 · depth 16
• Transitivity of the Galois group on valuation rings over O ValuationSubring.exists_algEquiv_forall_mem_iff_of_isGalois 2 below · cited by 1 · depth 16
• Tame inertia characters of exponent m are powers of the tame character ValuationSubring.exists_eq_tameCharacter_pow_of_pow_eq_one 18 below · cited by 1 · depth 16
• Relative Frobenius at a place of ℚ̄ over a number field ValuationSubring.exists_forall_apply_eq_and_isFrobeniusAt_natCard_of_liesOverPrime 2 below · cited by 5 · depth 16
• Descent of p^N-th powers along inertia for odd p ValuationSubring.exists_forall_mem_inertiaSubgroupIn_apply_eq_and_pow_eq_pow_of_isPrimitiveRoot 1 below · cited by 1 · depth 16
• Inertia-invariant Kummer class has an inertia-fixed radicand ValuationSubring.exists_inertia_fixed_radicand_of_kummer_class_invariant 1 below · cited by 1 · depth 16
• Additive inertia characters are Kummer characters ValuationSubring.exists_kummer_generator_of_additive_inertia_character 4 below · cited by 1 · depth 16
• Inertia-field valuation ring: a DVR with uniformiser p ValuationSubring.exists_ringHom_comap_fixedField_inertiaSubgroupIn_comp_eq_and_isDiscreteValuationRing 6 below · cited by 4 · depth 16
• Transcendental residue forces value group of 𝒪 to equal that of A ValuationSubring.exists_smul_mem_of_transcendental_residue 0 below · cited by 1 · depth 16
• Commensurability of valuations on a field algebraic over ℚ ValuationSubring.exists_valuation_pow_eq_valuation_zpow_of_isAlgebraic 1 below · cited by 7 · depth 16
• Units in residue fields of places of ℚ̄ are torsion ValuationSubring.isOfFinOrder_units_residueField_of_liesOverPrime 0 below · cited by 3 · depth 16
• Elementwise criterion for membership in the inertia subgroup ValuationSubring.mem_inertiaSubgroup_map_subtype_iff 0 below · cited by 2 · depth 16
• Conjugacy of valuation rings of ℚ̄ with the same residue prime ValuationSubring.exists_algEquiv_forall_mem_iff_of_nonunits 1 below · cited by 2 · depth 17
• Frobenius powers on residues realised in Gal(ℚ̄/K) ValuationSubring.exists_algEquiv_residue_pow_eq_of_nonunits 1 below · cited by 2 · depth 17
• Valuation rings over O versus maximal ideals of the integral closure ValuationSubring.exists_isMaximal_valuation_lt_one_iff_and_exists_of_isMaximal_integralClosure 0 below · cited by 3 · depth 17
• Value group is torsion over that of an algebraic subfield ValuationSubring.exists_pow_valuation_eq_valuation_algebraMap_of_isAlgebraic 0 below · cited by 5 · depth 17
• Value group over ℚ is divisible-hull generated by v(p) ValuationSubring.exists_pow_valuation_eq_valuation_natCast_zpow_of_isAlgebraic 1 below · cited by 4 · depth 17
• Existence of the Gauss prolongation to L(X) ValuationSubring.exists_regularProlongation_ratFunc 0 below · cited by 2 · depth 17
• Residues of a place of ℚ̄ come from its inertia field ValuationSubring.exists_residue_algebraMap_fixedField_inertiaSubgroupIn_eq 0 below · cited by 8 · depth 17
• Residue ring at a valuation centre is 𝔽ₚ[X] ValuationSubring.exists_ringEquiv_quotient_polynomial_zmod_of_residue_generated 2 below · cited by 1 · depth 17
• Valuation of a is a rational power of v(varpi) strictly inside the annulus ValuationSubring.exists_valuation_pow_eq_valuation_pow_of_mul_eq_pow_of_lt_one 2 below · cited by 2 · depth 17
• Completion of ℚ̄ at a place above p is algebraically closed ValuationSubring.isAlgClosed_completion_of_liesOverPrime 4 below · cited by 35 · depth 17
• Inertia-fixed part of a place above ℓ is a DVR with uniformiser ℓ ValuationSubring.isDiscreteValuationRing_comap_fixedField_inertiaSubgroupIn 4 below · cited by 30 · depth 17
• Valuation rings over O as localisations of the integral closure ValuationSubring.mem_iff_exists_integralClosure_valuation_eq_one_mul_eq_of_isAlgebraic 0 below · cited by 4 · depth 17
• Frobenius raises roots of unity of order prime to q to the q-th power ValuationSubring.smul_eq_pow_of_isFrobeniusAt_of_pow_eq_one 0 below · cited by 4 · depth 17
• Discreteness: iterated q-th roots of values of a number field are trivial ValuationSubring.valuation_seq_eq_one_of_forall_pow_eq_of_finiteDimensional 0 below · cited by 1 · depth 17
• Valuation subrings over a DVR pinned by separable approximants ValuationSubring.eq_of_forall_exists_sub_valuation_lt_one 0 below · cited by 1 · depth 18
• Roots lift along the residue map of a valuation subring ValuationSubring.exists_eval_eq_zero_and_residue_eq 0 below · cited by 2 · depth 18
• Completion of an algebraically closed field at a rank-one valuation ValuationSubring.isAlgClosed_completion_of_mulArchimedean_valueGroup 0 below · cited by 1 · depth 18
• Integrality from valuation rings of F with trace V ValuationSubring.isIntegral_of_forall_mem 0 below · cited by 2 · depth 18
• Valuation subrings over a DVR in a separable extension are discrete with uniformiser π ValuationSubring.isPrincipalIdealRing_and_maximalIdeal_eq_span_of_irreducible 0 below · cited by 1 · depth 18
• Unit discriminant gives 𝒪[c] as the integral closure ValuationSubring.mem_adjoin_singleton_of_isIntegral_of_isUnit_norm_aeval_derivative_minpoly 0 below · cited by 1 · depth 18
• Value group of a place above p in ℚ̄ is archimedean ValuationSubring.mulArchimedean_valueGroup_of_isAlgebraic_of_valuation_natCast_lt_one 2 below · cited by 14 · depth 18
• Degree of the reduction equals the number of integral roots ValuationSubring.natDegree_map_eq_card_roots_of_splits 0 below · cited by 1 · depth 18
• The rational closure inside the completion has a discrete valuation ring of integers ValuationSubring.exists_isDiscreteValuationRing_isFractionRing_ratClosure_finite_residueField_and_irreducible_natCast_of_liesOverPrime 1 below · cited by 5 · depth 19
• Tame Kummer character of inertia valued in ℤ/m ValuationSubring.exists_monoidHom_inertiaSubgroupIn_multiplicative_zmod_surjective_forall_apply_eq_pow_mul_of_isPrimitiveRoot 13 below · cited by 1 · depth 19
• Residue field K persists along algebraic extensions of valuation rings ValuationSubring.exists_sub_algebraMap_mem_nonunits_of_isAlgebraic 0 below · cited by 1 · depth 19
• Henselianity of the valuation ring of the inertia field ValuationSubring.henselianLocalRing_comap_fixedField_inertiaSubgroupIn 1 below · cited by 16 · depth 19
• Isotropy of a μ-type subset for an inertia-equivariant q^k-th-root pairing, q odd ValuationSubring.pairing_eq_one_of_inertia_smul_eq_nsmul_of_ne_two 1 below · cited by 1 · depth 19
• Unique integral root lifting a simple root of the reduction ValuationSubring.existsUnique_isRoot_residue_eq_of_rootMultiplicity_map_residue_eq_one 0 below · cited by 1 · depth 20
• Places of ℚ̄ above p are conjugate, compatibly with residue isomorphisms ValuationSubring.exists_algEquiv_smul_eq_and_residue_eq_of_ringEquiv_residueField 2 below · cited by 2 · depth 20
• Nontrivial characters of (ℤ/m)^× detect inertia at q ValuationSubring.exists_mem_inertiaSubgroupIn_cycloChar_ne_one 2 below · cited by 1 · depth 20
• Surjective tame Kummer character of inertia at r ValuationSubring.exists_monoidHom_inertiaSubgroupIn_rootsOfUnity_surjective_forall_apply_eq_mul_of_pow_eq_of_not_dvd 12 below · cited by 1 · depth 20
• Teichmüller lift of a finite-field embedding into mathcal O_P ValuationSubring.exists_units_monoidHom_residue_eq_of_injective_of_card_eq_prime_pow 3 below · cited by 2 · depth 20
• Valuation rings of finite Krull dimension have finite spectrum ValuationSubring.finite_primeSpectrum_of_ringKrullDim_lt_top 0 below · cited by 1 · depth 20
• Finiteness of the residues of A ∩ L in κ(A) ValuationSubring.finite_range_residue_of_nonunits 1 below · cited by 1 · depth 20
• Compactness of closed balls in the rational closure ValuationSubring.isCompact_ratClosure_inter_closedBall_of_liesOverPrime 3 below · cited by 3 · depth 20
• Closure of ℚ in a completion of ℚ̄ over r is a DVR with uniformiser r ValuationSubring.isDiscreteValuationRing_valuationSubring_ratClosure_and_irreducible_natCast_and_finite_quotient_of_liesOverPrime 0 below · cited by 2 · depth 20
• Residue field at a place of ℚ̄ is ̄mathbb F_{q²} ValuationSubring.nonempty_residueField_algEquiv_algebraicClosure_galoisField 0 below · cited by 6 · depth 20
• Krull dimension of a residue valuation ring between two primes ValuationSubring.ringKrullDim_residueValuationSubring_ofPrime_eq_krullDim_Icc 0 below · cited by 1 · depth 20
• Rank one of the completion of ℚ̄ over r ValuationSubring.valuation_completion_ratClosure_natCast_pos_and_lt_one_and_rankOne_of_liesOverPrime 3 below · cited by 18 · depth 20
• Inertia above 2 realises every unit of ℤ/8 on μ₈ ValuationSubring.exists_mem_inertiaSubgroupIn_apply_eq_pow_of_pow_eight_eq_one 0 below · cited by 1 · depth 21
• ℚᵣ as the closure of ℚ in widehatℚ̄_A ValuationSubring.exists_ringEquiv_adicCompletion_ratClosure_of_liesOverPrime 3 below · cited by 4 · depth 21
• Fraction field of k⊗_A V identified with E' ValuationSubring.exists_fractionRing_tensorProduct_quotient_algEquiv_apply_tmul_eq_coeffMap_of_residueField_ringEquiv 0 below · cited by 2 · depth 22
• Places of ℚ̄ above p come from p-adic embeddings ValuationSubring.exists_intermediateField_ringHom_padicAlgCl_of_liesOverPrime_of_finiteDimensional 7 below · cited by 1 · depth 22
• Inertia at p surjects onto Gal(ℚ(ζₚ)/ℚ) ValuationSubring.exists_mem_inertiaSubgroupIn_forall_apply_algebraMap_eq_of_isCyclotomicExtension 4 below · cited by 2 · depth 22
• Inertia element with trivial tame character moving a λ-th root of π ValuationSubring.exists_mem_inertiaSubgroupIn_tameCharacter_eq_one_and_pow_eq_and_apply_ne 15 below · cited by 3 · depth 22
• Place-stabilising ring automorphisms as inertia elements of trivial tame character ValuationSubring.exists_mem_inertiaSubgroupIn_tameCharacter_eq_one_coe_eq_of_ringEquiv 0 below · cited by 3 · depth 22
• Rank one of valuations on ℚ̄ ValuationSubring.exists_valuation_pow_le_of_mem_maximalIdeal_algebraicClosure_rat 2 below · cited by 3 · depth 22
• Henselianity of A ∩ L^I for I inside inertia ValuationSubring.henselianLocalRing_inf_fixedField_of_le_inertiaSubgroupIn 1 below · cited by 8 · depth 22
• Uncountability of the r-adic upper half plane over C_A ValuationSubring.not_countable_upperHalfPlane_ratClosure_completion_of_liesOverPrime 8 below · cited by 3 · depth 22
• Residue valuation detects the maximal ideal of A ValuationSubring.residueValuationSubring_valuation_lt_one_iff 0 below · cited by 1 · depth 22
• Reduction P∩ℚ̄^I→κ(P) is surjective; unit criterion ValuationSubring.surjective_residue_comp_inclusion_inf_fixedField_and_isUnit_iff_of_le_inertiaSubgroupIn 1 below · cited by 1 · depth 22
• Kernel, conjugates and values of the level-two tame character ValuationSubring.tameCharacter_eq_one_iff_apply_eq_and_conj_mem_and_exists_apply_eq_of_pow_sq_sub_one_eq 0 below · cited by 20 · depth 22
• Inertia with trivial tame character fixes q-th roots of unity ValuationSubring.apply_eq_self_of_pow_eq_one_of_tameCharacter_eq_one 6 below · cited by 10 · depth 23
• A uniform tame generator of inertia modulo p^m-th powers ValuationSubring.exists_forall_tame_generator_inertiaSubgroupIn 2 below · cited by 2 · depth 23
• Tame generator of inertia fixing a subfield L ValuationSubring.exists_forall_tame_generator_inertiaSubgroupIn_of_forall_apply_algebraMap_eq 3 below · cited by 1 · depth 23
• Centre of a valuation ring dominating a DVR ValuationSubring.exists_ideal_integralClosure_eq_valuationSubringAtPrime_and_inertiaDeg_eq_finrank 0 below · cited by 3 · depth 23
• Inertia elements lift along normal subextensions ValuationSubring.exists_mem_inertiaSubgroupIn_restrictNormal_eq 3 below · cited by 1 · depth 23
• Rational powers of a pseudo-uniformiser in a valuation ring ValuationSubring.exists_pow_eq_unit_mul_zpow_of_isAlgebraic_of_isNoetherianRing 1 below · cited by 1 · depth 23
• Powers of v(r) are coinitial in the value group ValuationSubring.exists_pow_valuation_ratClosure_natCast_le_of_liesOverPrime 4 below · cited by 1 · depth 23
• Two closed subfields of ℂ_A meeting in ℚ̄^{ cl} ValuationSubring.exists_two_closed_subfields_completion_inf_eq_ratClosure_of_liesOverPrime 7 below · cited by 1 · depth 23
• Automorphism fixing π and preserving A scales by units ValuationSubring.exists_unit_apply_eq_mul_of_mem_iff_apply_mem_of_rankOne 0 below · cited by 4 · depth 23
• Inertia-fixed elements of widehatℚ̄ᵥ: valuations and n-th roots ValuationSubring.exists_valuation_eq_zpow_and_exists_pow_eq_of_forall_inertia_smul_completion_eq 10 below · cited by 1 · depth 23
• Finite window and valuation-adapted basis for an independent family ValuationSubring.exists_window_and_adapted_basis 0 below · cited by 1 · depth 23
• Endomorphisms with trivial reduction move Gauss-presented rings inside 𝔪 ValuationSubring.mem_and_sub_mem_maximalIdeal_of_gaussPresentation_of_coe_eq_of_coeffMap_residue_comp_eq 0 below · cited by 5 · depth 23
• Archimedean value group versus powers in the maximal ideal ValuationSubring.mulArchimedean_valueGroup_iff_forall_exists_pow_le 0 below · cited by 9 · depth 23
• Uniqueness of the valuation ring above W₀ in a constants tower ValuationSubring.eq_of_constantsTower_of_forall_mem_iff 1 below · cited by 22 · depth 24
• Admissible small constants for a valuation ring above q ValuationSubring.exists_admissible_smallConstants 20 below · cited by 1 · depth 24
• Admissible small constants stable under the decomposition group ValuationSubring.exists_admissible_smallConstants_stable 19 below · cited by 2 · depth 24
• Extending a valuation along a totally ramified constant field extension ValuationSubring.exists_constantsTower_of_totallyRamified_of_isIntegral 0 below · cited by 14 · depth 24
• Weierstrass preparation over a henselian valuation ring ValuationSubring.exists_eq_units_mul_prod_sub_algebraMap_of_notMem_map_maximalIdeal 3 below · cited by 1 · depth 24
• Inertia at a place over v moves a p₀-th root ValuationSubring.exists_forall_mem_asIdeal_iff_mem_inertiaSubgroupIn_fixing_ne_of_not_dvd_valuation 0 below · cited by 1 · depth 24
• A uniform tame generator of inertia above q ValuationSubring.exists_forall_tame_generator_inertiaSubgroupIn_of_isGalois 2 below · cited by 1 · depth 24
• Decomposition group surjects onto residue automorphisms (Hilbert–Krull) ValuationSubring.exists_mem_decompositionSubgroup_forall_residue_smul_eq 0 below · cited by 2 · depth 24
• Quadratic Frobenius-parity character of a decomposition group at r ValuationSubring.exists_monoidHom_decompositionSubgroup_zmod_two_eq_one_of_mem_inertiaSubgroupIn_ne_one_of_isFrobeniusAt 3 below · cited by 2 · depth 24
• Galois conjugacy of valuation subrings over a common restriction ValuationSubring.exists_smul_eq_of_forall_algebraMap_mem_iff_of_isGalois 2 below · cited by 4 · depth 24
• A henselian tame descent base containing π with π^{q^2-1}=q ValuationSubring.exists_subfield_henselian_isDiscreteValuationRing_inf_of_liesOverPrime 17 below · cited by 3 · depth 24
• Uniform p-power window for a nonzero algebraic number ValuationSubring.exists_uniform_pow_mul_mem_of_liesOverPrime 0 below · cited by 4 · depth 24
• Fundamental identity sum_B e(B∣ A)f(B∣ A)=[F:K] ValuationSubring.finsum_ramificationIdx_mul_inertiaDeg_eq_finrank 0 below · cited by 6 · depth 24
• Ax–Sen–Tate: invariants in ℂₚ of a subgroup ValuationSubring.forall_smul_completion_eq_self_iff_mem_closure 1 below · cited by 1 · depth 24
• Totally ramified layers over a henselian discrete valuation ring ValuationSubring.isIntegral_and_exists_totallyRamified_layers_of_henselian 3 below · cited by 29 · depth 24
• Fraction field of k⊗_A V at a minimal prime is E' ValuationSubring.nonempty_fractionRing_tensorProduct_quotient_algEquiv_of_residueField_ringEquiv_of_linearIndependent 0 below · cited by 2 · depth 24
• Residue part of the fundamental inequality for valuation prolongations ValuationSubring.sum_finrank_residueField_le_finrank_of_forall_mem_iff 0 below · cited by 5 · depth 24
• Inertia acts trivially on the residue field of the completion ValuationSubring.valuation_completion_smul_sub_self_lt_one_of_mem_inertiaSubgroup 0 below · cited by 1 · depth 24
• Valuation of a rational is 1 iff v_q(r)=0 ValuationSubring.valuation_ratCast_eq_one_iff_padicValRat_eq_zero 4 below · cited by 26 · depth 24
• Uniqueness of a valuation subring extension via residue independence ValuationSubring.eq_of_comap_eq_of_forall_sum_mul_not_mem_nonunits 0 below · cited by 1 · depth 25
• Admissible small constants over a valuation ring above q=3 ValuationSubring.exists_admissible_smallConstants_of_eq_three 20 below · cited by 1 · depth 25
• Admissible small constants over a valuation ring above q=2 ValuationSubring.exists_admissible_smallConstants_of_eq_two 20 below · cited by 1 · depth 25
• Decomposition-stable admissible small constants for q=3 ValuationSubring.exists_admissible_smallConstants_stable_of_eq_three 19 below · cited by 2 · depth 25
• Decomposition-stable admissible small constants for q=2 ValuationSubring.exists_admissible_smallConstants_stable_of_eq_two 19 below · cited by 2 · depth 25
• Existence of tame-fixed admissible small constants over A ValuationSubring.exists_admissible_smallConstants_tameFixed 27 below · cited by 1 · depth 25
• A henselian DVR in the inertia field above ℓ ValuationSubring.exists_dvr_henselian_inertiaField_of_liesOverPrime 10 below · cited by 2 · depth 25
• Residual transcendence descends to an algebraic subfield ValuationSubring.exists_forall_isUnit_polynomialEval2_comap_of_residuallyNonconstant 0 below · cited by 3 · depth 25
• Witt vectors of 𝔽̄ₚ inside a completion at a place over p ValuationSubring.exists_isAlgClosed_wittVector_ringHom_completion_of_liesOverPrime 4 below · cited by 1 · depth 25
• Finite layers of a valuation ring algebraic over a DVR ValuationSubring.exists_layer_isDiscreteValuationRing_of_finite_of_isAlgebraic_of_irreducible 2 below · cited by 2 · depth 25
• Radical-fixing inertia elements are pⁿ-th powers in inertia ValuationSubring.exists_mem_inertiaSubgroupIn_pow_eq_of_forall_apply_eq_of_isGalois 1 below · cited by 1 · depth 25
• Nonzero values are attained in the valued completion ValuationSubring.exists_ne_zero_and_v_le_of_liesOverPrime 0 below · cited by 2 · depth 25
• Tame ℓ-adic exponent of an automorphism fixing π ValuationSubring.exists_padicInt_forall_apply_eq_pow_appr_mul_of_pow_eq_of_residue_eq 0 below · cited by 1 · depth 25
• Inertia-fixed lifts of residue classes in a valuation subring of ℚ̄ ValuationSubring.exists_residue_eq_and_forall_mem_inertiaSubgroupIn_apply_eq_of_liesOverPrime 2 below · cited by 7 · depth 25
• Inertia-field valuation ring over ℚ(ζₚ) is unramified DVR ValuationSubring.exists_ringHom_comap_fixedField_inertiaSubgroupIn_inf_fixingSubgroup_comp_eq_and_isDiscreteValuationRing_and_map_maximalIdeal_eq 3 below · cited by 2 · depth 25
• Lifting points of a finite flat algebra to a valuation subring ValuationSubring.exists_ringHom_comp_eq_of_moduleFinite_of_flat 0 below · cited by 2 · depth 25
• Transfer of genericity along monic relations between J and J' ValuationSubring.forall_aeval_mem_and_inv_mem_of_isRoot_of_isRoot 0 below · cited by 5 · depth 25
• The decomposition ring of a place of ℚ̄ over ℓ ValuationSubring.henselianLocalRing_and_exists_residue_zmod_inf_fixedField_decompositionSubgroup 9 below · cited by 6 · depth 25
• Residue field of the inertia ring of a place of ℚ̄ is algebraically closed ValuationSubring.isAlgClosed_residueField_comap_fixedField_inertiaSubgroupIn 2 below · cited by 11 · depth 25
• Finite layers over a henselian discrete valuation subring ValuationSubring.isDiscreteValuationRing_and_henselianLocalRing_comap_of_finiteDimensional 6 below · cited by 5 · depth 25
• The decomposition ring of a place of ℚ̄ over ℓ ValuationSubring.isDiscreteValuationRing_inf_fixedField_decompositionSubgroup 5 below · cited by 6 · depth 25
• Unique extension of a henselian discrete valuation ValuationSubring.toSubring_eq_integralClosure_and_finite_and_isDiscreteValuationRing_of_henselian 2 below · cited by 3 · depth 25
• Admissible small constants at q=3, tamely fixed ValuationSubring.exists_admissible_smallConstants_tameFixed_of_eq_three 27 below · cited by 1 · depth 26
• Admissible small constants, tame-fixed, at q = 2 ValuationSubring.exists_admissible_smallConstants_tameFixed_of_eq_two 27 below · cited by 1 · depth 26
• Common geometric element for finitely many discrete valuation subrings ValuationSubring.exists_forall_mem_and_forall_isUnit_polynomialEval2_of_finset_of_isDiscreteValuationRing 1 below · cited by 1 · depth 26
• Finite henselian levels inside a valuation subring ValuationSubring.exists_intermediateField_finiteDimensional_henselianLocalRing_comap_of_henselianLocalRing 8 below · cited by 2 · depth 26
• Valuation subring of O dominating a local subring of O ValuationSubring.exists_le_and_le_toLocalSubring_of_toSubring_le 0 below · cited by 9 · depth 26
• Wild inertia: a normal p-subgroup with abelian quotient ValuationSubring.exists_normal_isPGroup_commutator_le_inertiaSubgroup 2 below · cited by 1 · depth 26
• Abstract presentations of the valuation subring A ∩ k₀ ValuationSubring.exists_ringEquiv_comap_of_range_eq_inter 0 below · cited by 9 · depth 26
• Exact pencil: a finite set of Gauss components is realised ValuationSubring.exists_transcendental_forall_over_gauss_iff_mem_of_henselianLocalRing 102 below · cited by 1 · depth 26
• Two divisors of m in 𝔪 with distinct values ValuationSubring.exists_two_mem_maximalIdeal_dvd_valuation_ne_of_isAlgClosed 0 below · cited by 3 · depth 26
• Henselian discretely valued trace: faithfully flat integral prolongation ValuationSubring.faithfullyFlat_and_isIntegral_of_henselianLocalRing_comap 4 below · cited by 16 · depth 26
• Residually transcendental element gives a Gauss valuation subring ValuationSubring.inv_mem_and_chartAlg_le_and_over_gauss_and_isDiscreteValuationRing_of_forall_isUnit_polynomialEval2 6 below · cited by 3 · depth 26
• Inertia field of a place over ℚ(ζₚ) is unramified ValuationSubring.isDiscreteValuationRing_comap_fixedField_inertiaSubgroupIn_inf_fixingSubgroup_and_exists_mul_of_mem_maximalIdeal 1 below · cited by 1 · depth 26
• Krull–Akizuki: valuation subrings over one-dimensional Noetherian domains ValuationSubring.isDiscreteValuationRing_of_algebraMap_mem_of_finite 1 below · cited by 22 · depth 26
• Geometric elements avoid residually algebraic dominated subrings ValuationSubring.not_mem_and_inv_not_mem_of_dominates_of_residuallyAlgebraic_of_forall_isUnit_polynomialEval2 0 below · cited by 1 · depth 26
• Points of a module-finite algebra lie in a valuation subring ValuationSubring.algHom_apply_mem_of_moduleFinite 0 below · cited by 3 · depth 27
• Discrete valuation subrings have no proper overrings ValuationSubring.eq_or_eq_top_of_toSubring_le_of_isDiscreteValuationRing 0 below · cited by 7 · depth 27
• Uniformiser congruence subgroup of inertia is normal with abelian quotient ValuationSubring.exists_normal_commutator_mem_of_isDiscreteValuationRing 0 below · cited by 1 · depth 27
• A tame auxiliary prime ℓ and a qℓ-th root of unity ValuationSubring.exists_prime_isUnit_mul_sq_sub_one_and_isPrimitiveRoot_mul_of_henselian 0 below · cited by 1 · depth 27
• A p-adically complete target for all local evaluations into A ValuationSubring.exists_ringHom_forall_eq_mul_units_and_forall_exists_ringHom_adicCompletion_comp_eq_of_liesOverPrime 4 below · cited by 2 · depth 27
• Conjugacy of extensions and order ef of the decomposition group ValuationSubring.exists_smul_eq_and_card_stabilizer_eq_ramificationIdx_mul_inertiaDeg 0 below · cited by 1 · depth 27
• Wild inertia is a p-group at a discrete place ValuationSubring.isPGroup_of_forall_mem_iff_smul_sub_mem_sq 0 below · cited by 1 · depth 27
• Membership in a valuation ring centred on a prime varpi ValuationSubring.mem_iff_exists_not_dvd_of_prime_of_forall_mem_maximalIdeal_iff_dvd 0 below · cited by 1 · depth 27
• Finite fields of characteristic p embed into residue fields above p ValuationSubring.nonempty_ringHom_residueField_of_finite_of_charP 2 below · cited by 6 · depth 27
• Valuation ring of F inducing V on T and A on K ValuationSubring.exists_forall_mem_iff_of_forall_eq_of_agree 0 below · cited by 3 · depth 28
• Frobenius at a place of ℚ̄ and wild commutators with inertia ValuationSubring.exists_isFrobeniusAt_pow_forall_inertiaSubgroupIn_conj_mul_pow_inv_wild 10 below · cited by 1 · depth 28
• Discrete place under a finite group action: Dedekind data ValuationSubring.exists_mulSemiringAction_integralClosure_inf_fixedPoints_of_isDiscreteValuationRing 0 below · cited by 4 · depth 28
• Local lift of R to a valuation subring of ℚ̄ ValuationSubring.exists_ringHom_comp_eq_and_subtype_comp_eq_and_isLocalHom_of_isDiscreteValuationRing 5 below · cited by 2 · depth 28
• Descent of unit multiples from the I-adic completion of a valuation ring ValuationSubring.exists_units_eq_mul_of_algebraMap_adicCompletion_eq_mul_of_isUnit 0 below · cited by 1 · depth 28
• Residue fields of valuation subrings of ℚ̄ are algebraic over mathbb Fₚ ValuationSubring.forall_exists_pow_prime_pow_eq_self_residueField 0 below · cited by 1 · depth 28
• Descent of the centred valuation ring to the fixed subfield ValuationSubring.forall_mem_comap_iff_of_centred_of_isInvariant 0 below · cited by 1 · depth 28
• Henselian valuation rings extend uniquely to algebraic extensions ValuationSubring.forall_mem_iff_isIntegral_and_eq_of_henselianLocalRing 4 below · cited by 4 · depth 28
• Proper valuation subring of ℚ̄ meets a number field in a DVR ValuationSubring.isDiscreteValuationRing_inf_toSubring_of_ne_top 2 below · cited by 1 · depth 28
• Valuation subrings over a DVR in finite separable extensions ValuationSubring.isDiscreteValuationRing_of_forall_algebraMap_mem_of_isSeparable 0 below · cited by 1 · depth 28
• Inertia order equals ramification index for a discrete place ValuationSubring.map_maximalIdeal_comap_fixedPoints_eq_maximalIdeal_pow_card_inertia 3 below · cited by 2 · depth 28
• Ramification index equals inertia order at every conjugate ValuationSubring.map_maximalIdeal_comap_fixedPoints_eq_pow_of_eq_smul_of_natCard_eq 4 below · cited by 1 · depth 28
• Decomposition ring of a place of ℚ̄ maps into any henselian dominating local domain ValuationSubring.mem_range_algebraMap_of_mem_inf_fixedField_decompositionSubgroup_of_henselianLocalRing 13 below · cited by 1 · depth 28
• Embeddings inducing a given valuation ring number ef ValuationSubring.natCard_algHom_comap_eq_ramificationIdx_mul_inertiaDeg 0 below · cited by 1 · depth 28
• Inertia at an ideal fixes the valuation subring centred on it ValuationSubring.smul_eq_and_forall_smul_sub_mem_nonunits_of_mem_inertia 0 below · cited by 1 · depth 28
• Independence of the tame character from the chosen root of q ValuationSubring.tameCharacter_eq_tameCharacter_of_pow_sq_sub_one_eq_of_mem_inertiaSubgroupIn 0 below · cited by 3 · depth 28
• Extensions of valuations to algebraic extensions come from embeddings ValuationSubring.exists_algHom_forall_apply_mem_iff_of_isAlgebraic 4 below · cited by 1 · depth 29
• Étale ℤ-algebra neighbourhoods exhaust the decomposition ring ValuationSubring.exists_etale_int_ringHom_apply_eq_of_mem_inf_fixedField_decompositionSubgroup 10 below · cited by 1 · depth 29
• Lifting inertia along a normal extension ValuationSubring.exists_mem_inertiaSubgroupIn_and_forall_apply_algebraMap_eq 0 below · cited by 1 · depth 29
• Unique discrete place centred on a maximal ideal ValuationSubring.exists_unique_centred_of_isDiscreteValuationRing_of_isFractionRing 0 below · cited by 1 · depth 29
• Prime-to-n radicand: unique, totally ramified extension of O ValuationSubring.forall_comap_eq_imp_eq_and_exists_forall_sub_mem_nonunits_of_pow_eq_of_isCoprime 5 below · cited by 1 · depth 29
• Residual transcendence transfers between mutually integral elements ValuationSubring.forall_monic_aeval_not_mem_maximalIdeal_iff_of_isIntegral_adjoin 0 below · cited by 13 · depth 29
• Valuation rings of A-integral q-expansions are discrete ValuationSubring.isDiscreteValuationRing_of_forall_mem_iff_gaussPresentation 0 below · cited by 4 · depth 29
• ℚ̄ is 𝒪 localised away from p ValuationSubring.isLocalization_away_natCast_of_liesOverPrime 0 below · cited by 1 · depth 29
• Descent of a DVR with invariant uniformiser to the fixed field ValuationSubring.maximalIdeal_comap_fixedPoints_eq_span_and_mem_iff_exists_invariant_of_isLocalization 4 below · cited by 8 · depth 29
• Pointwise fixing P∩ L^{D_P} forces membership in D_P ValuationSubring.mem_decompositionSubgroup_of_forall_apply_eq_of_mem_inf_fixedField 0 below · cited by 2 · depth 29
• Inertia of a place equals inertia of its centre, order e ValuationSubring.smul_eq_and_forall_smul_sub_mem_nonunits_iff_mem_inertia_and_card_eq_ramificationIdxIn 0 below · cited by 3 · depth 29
• Total ramification of finite layers over a varpi-centred valuation ring ValuationSubring.exists_eq_mul_pow_finrank_and_adjoin_simple_eq_of_forall_valuationSubring_eq 3 below · cited by 1 · depth 30
• Trace of a valuation ring on a finite layer: finiteness up to units ValuationSubring.exists_finset_forall_exists_mem_span_mul_eq_of_intermediateField_le 0 below · cited by 1 · depth 30
• Finite extension of ℚₚ containing ι(R_h) ValuationSubring.exists_intermediateField_finiteDimensional_forall_apply_mem_of_isDiscreteValuationRing_of_liesOverPrime 5 below · cited by 1 · depth 30
• Unramified descent of a discrete valuation ring to the fixed field ValuationSubring.isDiscreteValuationRing_comap_fixedPoints_and_exists_uniformizer_and_residue_descent 3 below · cited by 1 · depth 30
• Integral elements over a valuation ring lie in 𝒪[c] ValuationSubring.mem_adjoin_singleton_of_isIntegral_of_separable_minpoly 0 below · cited by 1 · depth 30
• Automorphisms fixing y stabilise the valuation ring W ValuationSubring.mem_iff_map_mem_of_ringEquiv_of_isLocalization_of_least_prime 0 below · cited by 2 · depth 30
• Valuation subring rigid under nonunit with radical maximal ideal ValuationSubring.eq_of_le_of_mem_nonunits_of_maximalIdeal_le_radical 0 below · cited by 4 · depth 31
• Local degree of ι(s) bounded by v_{R_h}(p) ValuationSubring.finrank_adjoin_image_le_addVal_of_isDiscreteValuationRing_of_liesOverPrime 3 below · cited by 1 · depth 31
• Pullback of a discrete valuation ring along a field embedding ValuationSubring.isDiscreteValuationRing_comap_of_mem_of_not_isUnit 0 below · cited by 3 · depth 31
• Galois transitivity on valuation rings over a DVR ValuationSubring.exists_algEquiv_comap_eq_of_isGalois 0 below · cited by 3 · depth 32
• Henselian DVR at the decomposition field over a finite extension ValuationSubring.exists_intermediateField_le_isDiscreteValuationRing_henselianLocalRing_comap_of_finiteDimensional 16 below · cited by 1 · depth 32
• Extending a DVR along a finitely generated field extension ValuationSubring.exists_isDiscreteValuationRing_dominates_of_adjoin_finset_eq_top 4 below · cited by 1 · depth 32
• A discrete valuation ring extends along a finite field extension ValuationSubring.exists_isDiscreteValuationRing_dominates_of_finiteDimensional 2 below · cited by 5 · depth 32
• Full decomposition group forces uniqueness of the prolongation ValuationSubring.eq_of_comap_eq_of_forall_mem_decompositionSubgroup 3 below · cited by 1 · depth 33
• Extending a DVR along a simple transcendental extension ValuationSubring.exists_isDiscreteValuationRing_dominates_of_transcendental_of_adjoin_eq_top 0 below · cited by 1 · depth 33
• Frobenius and wild monodromy at a valuation over a DVR ValuationSubring.exists_isFrobeniusAt_pow_forall_inertiaSubgroupIn_conj_mul_pow_inv_wild_of_isDiscreteValuationRing 11 below · cited by 1 · depth 33
• Residues of a place of ℚ̄ come from its inertia field ValuationSubring.exists_mem_fixedField_inertiaSubgroupIn_sub_mem_nonunits 1 below · cited by 1 · depth 33
• Unique extension to the algebraic closure implies henselian ValuationSubring.henselianLocalRing_comap_of_forall_comap_eq_imp_eq 0 below · cited by 1 · depth 33
• Inertia ring over a number field is an unramified DVR ValuationSubring.isDiscreteValuationRing_comap_fixedField_inertiaSubgroupIn_of_irreducible 4 below · cited by 1 · depth 33
• Separable subfields fixed by the decomposition group carry DVRs ValuationSubring.isDiscreteValuationRing_comap_of_forall_isSeparable_of_forall_smul_eq 6 below · cited by 1 · depth 33
• Fixing the separable decomposition field forces stabilisation of A ValuationSubring.mem_decompositionSubgroup_of_forall_mem_fixedField_inf_separableClosure_imp_eq 1 below · cited by 1 · depth 33
• Wild automorphisms act with p-power order on finite normal levels ValuationSubring.exists_forall_pow_prime_pow_apply_eq_of_wild_of_normal 1 below · cited by 1 · depth 34
• Inertia of a place of ℚ̄ surjects onto finite layers ValuationSubring.exists_ideal_ringOfIntegers_inertia_eq_map_restrictNormalHom_of_isGalois 0 below · cited by 1 · depth 34
• Existence of a Frobenius element over a finite subextension ValuationSubring.exists_isFrobeniusAt_pow_of_isDiscreteValuationRing 4 below · cited by 1 · depth 34
• Elements fixed by the decomposition group have values from K ValuationSubring.exists_ne_zero_and_div_mem_of_forall_smul_eq_imp_apply_eq 3 below · cited by 1 · depth 34
• Inertia-fixed elements have valuation a power of varpi ValuationSubring.exists_valuation_mul_zpow_eq_one_of_forall_inertia_apply_eq 2 below · cited by 1 · depth 34
• Discreteness descends to intermediate fields with the same values ValuationSubring.isDiscreteValuationRing_comap_of_forall_exists_div_mem_units 0 below · cited by 1 · depth 34
• A valuation subring over a DVR is a localisation of the integral closure ValuationSubring.integralClosure_le_and_exists_ideal_mem_iff_mem_nonunits_and_mem_iff_exists_of_isDiscreteValuationRing 0 below · cited by 1 · depth 35
• Hilbert theory for valuation rings in a finite Galois extension ValuationSubring.normal_residueField_and_forall_algEquiv_exists_smul_eq_of_isGalois 2 below · cited by 1 · depth 35
• Additivity of Krull dimension for a pair of valuation subrings ValuationSubring.ringKrullDim_eq_ringKrullDim_residueValuationSubring_add 0 below · cited by 1 · depth 35
• A place of ℚ̄ computes the Q-adic order ValuationSubring.valuation_eq_valuation_pow_of_mem_pow_of_not_mem_pow_succ 0 below · cited by 1 · depth 35
• Non-units transport along a ring map matching valuation subrings ValuationSubring.mem_nonunits_iff_map_mem_nonunits_of_forall_mem_iff 0 below · cited by 2 · depth 36
• Algebraically independent residues give no relations in mathfrak m_O ValuationSubring.eq_zero_of_valuation_eval2_lt_one 0 below · cited by 1 · depth 37
• Lifting d algebraically independent residues into a valuation ring ValuationSubring.exists_algebraicIndependent_residue_of_le_trdeg 0 below · cited by 1 · depth 37
• Residue field transcendence degree under restriction of a valuation ValuationSubring.le_trdeg_residueField_comap_of_le_trdeg_residueField 1 below · cited by 1 · depth 37
• Gauss-type valuation rings agree on L(x) ValuationSubring.mem_iff_mem_of_mem_adjoin_simple_of_forall_aeval_inv_mem 0 below · cited by 2 · depth 37
• Residue transcendence degree bounded by trdeg_K L ValuationSubring.trdeg_residueField_le_trdeg 0 below · cited by 1 · depth 38

ValuationSubring.IsFrobeniusAt 5

• Frobenius at q ≠ p raises p-th roots of unity to the q-th power ValuationSubring.IsFrobeniusAt.apply_rootOfUnity_eq_pow 0 below · cited by 6 · depth 6
• Frobenius raises m-th roots of unity to the q-th power ValuationSubring.IsFrobeniusAt.apply_eq_pow_of_pow_eq_one 0 below · cited by 21 · depth 10
• Frobenius at q raises p^k-th roots of unity to the q-th power ValuationSubring.IsFrobeniusAt.apply_eq_pow_of_pow_prime_pow_eq_one 0 below · cited by 2 · depth 10
• Frobenius acts as q-th power on roots of unity of order prime to q ValuationSubring.IsFrobeniusAt.apply_rootOfUnity_eq_pow_of_not_dvd 0 below · cited by 3 · depth 13
• Tame commutator relation between Frobenius and inertia ValuationSubring.IsFrobeniusAt.conj_mul_pow_inv_mem_inertiaSubgroupIn_and_wild 3 below · cited by 1 · depth 34