Valued field theory

Valuations, local fields and ramification theory. Covers extensions and completions, ramification filtrations, different ideals and local norm calculations.

Canonical aggregate generated by the reviewed rehome.

Public aggregate for logarithm and exponential series on local fields, including convergence, continuity, and applications to field units.

This file contains the pure natural-number cancellation steps used after local-field norm and value-group arguments have produced an lcm divisibility. It also contains the elementary p-adic valuation estimates used in th…

If every action difference is divisible by a scalar, averaging and then projecting away from the invariants makes the augmentation part divisible by the same scalar. No finite generation or topology is required.

The inverse character twist turns character eigenvectors into invariants. The standard averaging projection commutes with an actual intertwining map, so every eigenvector in its image has an eigenvector preimage.

This file packages the ramification-scaled principal-unit logarithm as a continuous homomorphism and extends it to field units with the unique uniformizer value forced by log p = 0.

For a complete discrete valuation with value group WithZero (Multiplicative ℤ) and finite residue field, this file constructs the ramification index e = vK(p) from the valuation itself. In mixed characteristic it then pr…

The logarithm on first principal units does not extend by killing a chosen uniformizer. Its uniformizer value must instead be chosen so that the distinguished rational prime has logarithm zero. This file isolates that al…

This module isolates the torsion and unit-decomposition argument used to prove that an extension of the principal-unit logarithm is determined by its value on a uniformizer.

Linear growth dominates the logarithmic denominator contribution, so a single integer lies strictly below every term of the resulting real sequence. The corresponding integer sequence using padicValNat therefore attains…

This file supplies the unconditional summability and regrouping step needed to evaluate the formal identity log ((1 + X) (1 + Y)) = log (1 + X) + log (1 + Y) in a complete discretely valued field whose normalized valuati…

This file evaluates the two formal composition identities used in the deep exponential–logarithm equivalence, on the sharp ramified convergence ball. The source lemmas below justify the Cauchy products and the unconditio…

This file supplies the topological part of the deep exponential–logarithm equivalence at the sharp ramified endpoint n > e / (p - 1). The algebraic construction of the maps is supplied by the preceding modules; here we p…

Aggregate for the LocalFieldTheory.Analytic.LogExpSeries folder.

The actual valuation topology makes the field automorphism and its inverse continuous. Consequently they commute with the total infinite sum defining the logarithm; no supplied convergence or comparison theorem is needed…

Establishes convergence and summability of the exponential series on sufficiently deep nonarchimedean ideals.

This module completes the formal logarithm core by identifying the basic-factor choices with pairs of finite position sets and evaluating their cardinality. The formal-series identities and the underlying position calcul…

This aggregate exposes the formal coefficient and choice-position API used by the local logarithm and exponential series.

This module packages the three possible nonzero monomial factors and their finite choice spaces.

This module derives the three coordinate and total-count equations satisfied by a choice of the basic factors in X + Y + XY.

This module constructs a basic-factor choice from its mixed and left position sets and proves the resulting position-count formulas.

This module solves the coordinate-count system and relates its solution to the label-count and multinomial choice spaces.

This module develops the formal composition identities between Mathlib's PowerSeries.log and PowerSeries.exp that are used by the local-field logarithm and exponential.

This module defines X + Y + XY, its logarithmic substitution, and the support description needed for the formal product formula.

Proves the formal combinatorial identities behind additivity of the logarithm on products of principal units.

Packages the convergent logarithm and exponential series as additive and multiplicative homomorphisms on their natural nonarchimedean domains.

Develops the valuation estimates showing that logarithm and exponential series are inverse on their common principal-unit domain.

Establishes convergence and summability of the logarithm series on the nonarchimedean open unit ball.

Restricts the exponential series to deep additive ideals and shows that its values lie in the corresponding principal-unit subgroups.

Restricts the logarithm series to principal units and places its values in the corresponding additive ideal.

Defines the logarithm and exponential series terms and proves the valuation estimates used in their convergence arguments.

An eventual upper bound on a convergent sequence remains an upper bound on its limit. The bound need not be nonzero or occur as a value of the valuation.

The concrete field action restricts to principal units. Its compatibility with the constructed p-adic scalars supplies the linear representation laws.

The value of the residue prime supplies the strict ramified convergence bound. No completeness or normalization of the integer-valued valuation is needed.

If v(x) < 1, the integer valuation of the nth logarithm term is at least n + 1 - e vp(n + 1). This bound is independent of x. The scale e and the denominator values are obtained from the actual residue prime.

Reduction modulo p^n maps to reduction modulo the nth maximal-ideal power. Adic completeness lifts these compatible maps to the actual valuation ring. Neither characteristic zero nor finiteness of the residue field is re…

The lifted map carries the open kernel of reduction modulo p^n into the nth maximal-ideal power. The adic topology on the valuation ring is its actual subtype topology, so the map to the field is continuous.

A valuation-preserving field automorphism fixes the constructed image of the p-adic integers, by continuity and density of the natural numbers.

The two maps agree on natural numbers. Their continuity in the actual valuation topologies extends this equality to all p-adic integers.

The logarithm is constructed on every complete mixed-characteristic discrete valuation field, including fields with infinite residue field. Its scale and the completeness of the actual valuation topology are supplied by…

The integer sequence n - e vp(n), for positive n, has an attained minimum. Every nonzero principal-unit logarithm has integer valuation at least that minimum. The bound is uniform over all principal units, including when…

A valuation-preserving field automorphism acts on the actual principal-unit group, and its field action commutes with the logarithm of that unit. Both the action and the continuity used to transport the infinite sum are…

Exponentiating p² a for an element a of the valuation ring produces an actual principal unit with logarithm p² a. The convergence threshold is proved from the valuation of the residue prime. No normalized uniformizer, fi…

Both scalar actions and their continuity are supplied by the preceding constructions. Density of natural exponents upgrades additivity of the logarithm to linearity over the p-adic integers.

The uniform lower bound on the integer valuations of logarithms gives a least valuation among the nonzero elements of any nonzero subgroup of the logarithm image. Dividing a least element by the residue prime strictly de…

The logarithm is linear for the canonical p-adic module structures and intertwines the actual valuation-preserving automorphisms. This supplies its image as a subrepresentation without any image-stability hypothesis.

First multiply an arbitrary field element by a power of the residue prime to make it integral. The existing exponential construction then realizes an additional factor of p² as the logarithm of an actual principal unit.

The field automorphism restricts continuously to valuation-ring units and principal units. The density theorem for continuous additive maps then supplies compatibility with the actual p-adic scalars.

The residue characteristic of the raw valuation supplies the characteristic of its bundled complete-DVF residue field. Scalar multiplication is then read multiplicatively as a p-adic power.

Reduction of a p-adic exponent modulo p^s changes its action on a principal unit by an actual p^s-th power. The witness is constructed in the principal unit group and then mapped into the field unit group.

An inverse-character weighted sum of the normal basis transforms by the character. Its coordinate at the identity automorphism is one, so the sum is nonzero, without any assumption on the characteristic or group order.

As in the normal-basis character eigenvector construction, inverse-character coefficients weight the actual canonical normal basis. Here the coefficients are supported only on a subgroup. This vector transforms by the ch…

A binomial expansion shows that the augmentation image of such an action on a torsion-free additive group is p-divisible. This does not require finite generation or any topology on the group.

This file combines the two evaluated formal composition identities with the valuation-theoretic endpoint maps and their continuity. No finite-quotient or defect-membership hypothesis remains in the public result.

The comparison uses the actual valuation topology and does not require a finite residue field. The valued-field structure is fixed once in the context.

Character eigenvectors are fixed points of the representation twisted by the inverse character. The same construction is shared by averaging and by restriction to invariant submodules.

Focused aggregate for valued-field basics, ramification invariants, norms, and unit filtrations.

A local-field package here is a chosen complete discretely valued field with finite residue field. The topology-first mathlib class remains available through imports; this file only adds the chosen-valuation API needed d…

This file starts the equal-characteristic branch of the local-field structure classification, the local-field structure classification. Given the Teichmuller coefficient-field section κ -> OK -> K and a uniformizer π, it…

This file connects mathlib's Algebra.norm with the unit-group and valued-norm APIs used by local CFT.

This file isolates the purely algebraic source for the Abhyankar norm-image argument: embedded base units, their powered image in a lower branch, and the image obtained after applying the lower norm. The only theorem use…

An algebra equivalence over the base field preserves the field norm and therefore identifies the corresponding norm subgroups of the base unit group.

This file connects the principal-unit decomposition proved in PrincipalUnits to the standard integer-valued field-unit valuation attached to a ℤᵐ⁰-valued complete discrete valuation.

This file isolates the two factors of the field-unit structure theorem which do not depend on the structure theorem for first principal units. The Teichmuller factor is the cyclic group of order q - 1, with its (necessar…

The index formulas below use the actual principal-unit structures from the field-unit structure theorem. Both the natural-cardinality form and the literal rational form involving the normalized local absolute value are r…

This file assembles the valuation, Teichmuller, and principal-unit factors in the canonical factor order. All topologies are the ones carried directly by the given WithZero (Multiplicative ℤ)-valued valuation.

This file starts the remaining equal-characteristic descent in the local-field structure classification: a finite coefficient field k of characteristic p gives a canonical coefficientwise map from Fp((X)) to k((X)).

The equal-characteristic proof naturally indexes copies of ℤ[p] by a positive integer prime to p and a residue-field basis vector. This file records that, when the basis is nonempty, this is exactly a countable product.

This module assembles the finite-level Iwasawa factors into a compatible family in the principal-unit inverse limit, proves continuity and bijectivity, and packages the resulting topological additive equivalence. This fi…

This file keeps the converse direction of the local-field structure theory, the local-field structure classification focused on the mixed-characteristic case. The key point proved here is that the actual range-restricted…

This aggregate exposes the mixed-characteristic structure, deep principal units, and integral lattice comparisons.

This module combines the deep free Zp lattice with the finite quotient exact sequence and packages the algebraic and topological structure of the first principal-unit group.

This module equips the canonical Zp lattice with the normalized valuation topology and transports integral-basis coordinates through the deep exponential--logarithm equivalence. equivalence

This file identifies the integer ring of a mixed-characteristic local field with the integral closure of the p-adic integers. In particular it supplies the finite free Zp lattice of rank [K : Qp] used in the proof of the…

Aggregate for the LocalFieldTheory.DiscreteValuationField.Norm folder.

This file contains the norm-subgroup lemmas used in local CFT from an abstract integer-valued multiplicative valuation and a norm homomorphism satisfying the standard valuation formula.

Develops quotient groups attached to an abstract valued norm, including kernel, image, and representative criteria. Identifies norm-quotient classes with valuation classes modulo the residue degree and constructs the res…

A compatibility hypothesis for a norm and two unit filtrations immediately produces homomorphisms on every filtration level.

This file is the first concrete example leaf for the DVF navigation library. It deliberately uses mathlib's public p-adic objects directly in theorem statements instead of introducing public aliases for ℚ[p] or its unit…

This is the density argument used explicitly in the local-field structure theory, the field-unit structure theorem: compatibility with ordinary integral powers, together with continuity of the p-adic scalar orbit, forces…

This file packages the PID step in the mixed-characteristic proof of the local-field structure theory, the field-unit structure theorem. Once the torsion submodule is known to be a finite cyclic group of order p^a, and t…

This is the free p-adic factor in the local-field structure theory, the local-field power-index formula. The exact equal-characteristic specialization, with no artificial finite factor in the principal-unit product.

The concrete local-field package on ℚ[p] uses the DVR valuation obtained from ℤ[p], whereas mathlib's nonarchimedean-local-field API uses ValuativeRel.valuation ℚ[p]. This file proves that these are equivalent valuations…

If a monic polynomial splits over a discrete valuation ring, one of its roots is at least as close to a given point as the polynomial value, after accounting for the derivative at that root. The proof selects a root of m…

This LubinTate consumer specializes the public commutative-group power-index API to the unit and principal-unit decompositions of a complete discrete valuation field.

This is the compactness step in the local-field structure theory, the equal-characteristic field-unit structure theorem. For a map from a compact space to the inverse limit lim U^1 / U^(n+1), surjectivity on every finite…

The coordinatewise p-adic action is transported across the canonical adic/prodiscrete comparison, producing its linear and topological forms on first principal units.

The adic topology on first principal units agrees with the prodiscrete topology carried by the inverse limit of finite quotient coordinates.

This aggregate exposes quotient and inverse-limit padic modules, their continuity, residue-characteristic actions, and prodiscrete topology comparisons.

Assembles the inverse-limit and topological models used to define the ℤ[p]-module structure on principal units.

Finite principal-unit quotients have the expected residue-characteristic exponent. Reduction of p-adic integers therefore supplies canonical module structures, compatible with the transition maps.

This file constructs the common source used in both cases of LubinTate, The field-unit structure theorem. A first principal unit is recovered from its classes in the level quotients U^1 / U^(n+1). For a local field these…

This module identifies first principal units algebraically and topologically with the inverse limit of their finite principal-unit quotients.

Reduction modulo p^n has open kernel and is continuous for the discrete topology on the quotient. This source has no local-field dependencies.

Taking a residue-characteristic power moves a positive principal-unit level one step deeper. Iteration kills U^1 / U^(n+1) by p^n, even when the residue field and the level quotients are infinite.

Coordinatewise scalar multiplication makes the prodiscrete inverse limit a topological module over the p-adic integers.

Reduction of scalars to ZMod (p^n) makes each coordinate action continuous. Density of natural scalars then proves compatibility with quotient reduction.

The exponent p^n of the level quotient supplies its ZMod (p^n) module. Reduction of p-adic integers then supplies the scalar action. These are explicit constructions, avoiding competing local-field instances.

These additive maps use the concrete principal-unit filtration of a complete discrete valuation field. Neither finiteness nor a scalar action is required.

The adic inverse-limit equivalence transports the compatible coordinate actions to U^1. No finite-residue-field assumption is used.

The compatible quotient actions define an action on the actual inverse-limit carrier. Its module laws and joint continuity follow coordinate by coordinate, without a finiteness assumption on the residue field.

Adic principal units, discrete finite quotients, and the prodiscrete inverse limit are represented by distinct wrapper types so that their topologies cannot be confused by instance selection. The algebraic quotient and i…

For a complete discrete valuation with value group WithZero (Multiplicative ℤ), the inherited topology agrees with the canonical adic model, so the p-adic action and addition are continuous on the original principal-unit…

This aggregate exposes the principal-unit filtration, residue quotients and roots, Teichmuller lifts and decomposition, and automorphism transport.

A field automorphism preserving the valuation ring restricts to every level of the principal-unit filtration, with its original action on field elements.

A field automorphism preserving the chosen valuation ring acts on the valuation ring, its residue field, its units, and every principal-unit quotient.

Develops quotients of valuation-ring units by higher principal units and compares their first layer with residue-field units.

For a complete DVF F, the concrete principal-unit filtration on the unit group of the valuation ring is U^n = { u | u - 1 ∈ m^n }. This file turns that definition into the abstract AntitoneSubgroupFiltration used by rami…

A field element whose p-power is a principal unit is represented by an actual element of the principal-unit subgroup, with the same power there. This is the root used when taking logarithms of a Kummer relation.

Identifies valuation-ring units modulo first principal units with residue-field units and records compatibility with valuation-preserving automorphisms.

Hensel lifting identifies the finite residue-field unit group with the lifted roots of unity in the valuation ring.

Decomposes valuation-ring units and field units into residue roots, first principal units, and a uniformizer factor.

Constructs multiplicative Teichmuller representatives, and in equal characteristic the coefficient-field section of the residue map.

The normalized additive valuation on the target valuation ring restricts to the ramification index times the normalized additive valuation on the base valuation ring. The proof is characteristic-independent and follows f…

This file records the ideal-theoretic source behind the local-field structure theory. The base maximal ideal maps to the e-th power of the target maximal ideal, where e is the canonical ramification index. Every statemen…

The ramification index and residue degree are the ideal-theoretic invariants of the chosen valuation rings. Every theorem below is stated directly in the ambient valued-extension context; there are no compatibility alias…

This file provides a theorem API for antitone principal-unit filtrations used by ramification and norm arguments.

This aggregate collects the range-restriction, integer-valuation, topology, uniformizer, and extension maps used for units of discrete valuation rings.

This file specializes multiplicative-range restriction to CompleteDVF and transports residue finiteness, adic completeness, cyclicity, and discreteness.

This file supplies the ordered-group and rank-one facts used for actual multiplicative valuation ranges, together with normalized uniformizer results for ℤᵐ⁰-valued valuations.

This file constructs the sign-normalized integer valuation on field units and proves the elementary formulas for powers and natural-number denominators.

This file relates the induced integer valuation to normalized uniformizers, valuation-ring units, and scalar extension of field units.

This file packages range restriction as a LocalField and exposes the properness and completeness of the resulting topology.

This file equips the multiplicative-range valuation with its valued and normed field structures and transports adic completeness, compactness, properness, and completeness.

The restricted valuation has the same valuation ring, maximal ideal, and residue field as the original valuation.

This file proves lower bounds and divergence-to-infinity statements for the integer valuations of the logarithm and exponential series terms.

A chosen uniformizer determines the exponent of every nonzero field value and therefore an integer-valued multiplicative valuation on field units.

This file defines the canonical homomorphism from units of a complete-DVF valuation ring to units of its fraction field.

This file proves compatibility of valuation-ring units with scalar extension and relates the value of an embedded base uniformizer to the ramification index.

This file contains the integer value-group subgroup-image lemmas used by the norm and ramification-image arguments. The results are purely about integer-valued multiplicative valuations and integer lcm divisibility.

This file transfers completeness from the actual-range restriction of a complete discrete valuation back to the topology obtained directly from Valued.mk' v.

Public aggregate for reusable power-subgroup and power-index APIs.

This module supplies the quotient equivalence induced by a continuous multiplicative equivalence. It belongs to the general local-field support layer and does not depend on the separate pro-\(C\) groups library.

Pure group-theoretic infrastructure for the subgroup of multiplicative integers divisible by a fixed integer and its cyclic quotient. It lives below the discrete-valuation-field layer so generic power-index code does not…

Reusable kernel, quotient, product, and additive-transport formulas for n-th powers in commutative groups. The basic power map and its image and kernel are mathlib's powMonoidHom, MonoidHom.range, and MonoidHom.ker.

Turns a multiplicative group equivalence into the corresponding equivalence between the additive recodings of its source and target.

Focused aggregate for valuations, residue extensions, finite unramified extensions, Frobenius, integer rings, principal units, continuous norm maps, and norm quotients of nonarchimedean local fields.

Compactness facts and the normalized integer-valued valuation attached to a nonarchimedean local field.

The canonical complete discrete valuation on a nonarchimedean local field, and an integral-closure valuation chosen on each finite separable extension.

This file packages the spectral norm topology on a finite extension of a nonarchimedean local field. The definitions are deliberately explicit: they let downstream constructions put several finite extensions in one diagr…

Develops the ideal, residue-field, Galois, trace, and norm consequences of a finite valued extension with ramification index one and full residue degree.

Integrality produces the integer-ring equivalence from the field equivalence. Transport of the actual maximal-ideal equality then preserves ramification index one. No valuation-preservation certificate is assumed: integr…

Restricts Galois automorphisms to valuation rings and transports their action to ideals, ideal-power quotients, principal units, and successive quotients.

This file packages the normalized valuation and the unit factor in the standard decomposition of Kˣ as continuous homomorphisms. After fixing a noncanonical uniformizer internally, the resulting parameter-free map lets d…

Packages field norms as homomorphisms on units and restricts them to valuation rings and their unit groups under the appropriate integral hypotheses.

This module records the analytic input used by the topological finite local reciprocity law: on a finite-dimensional normed algebra, the field norm is a determinant and is therefore continuous. It also bundles the corres…

Constructs Kˣ/N(Lˣ), its universal maps and comparison equivalences, and relates its finite cardinality to the index of the norm subgroup.

The local existence proof repeatedly enlarges a finite extension and replaces finite extensions by isomorphic realizations. This file records the resulting identities for unit norms and their images in the base field.

The Kummer branch of the local existence theorem uses power-class index formulas stated for valuations with value group WithZero (Multiplicative ℤ). A nonarchimedean local field carries its canonical valuation in an intr…

The multiplicative power-class group Kˣ / Kˣⁿ of a nonarchimedean local field is finite whenever n is nonzero in K. This is the finiteness input for maximal Kummer extensions and the characteristic-zero local existence t…

Transports valuation-ring automorphisms to maximal-ideal powers, principal units, and their successive quotients, together with the resulting actions.

Develops U^n/U^(n+1) and identifies it with the additive ideal quotient 𝓂^n/𝓂^(n+1) through the first-order map a ↦ 1 + a.

Defines the filtration U^n = 1 + 𝓂^n, proves its basic order properties, and constructs the quotient of valuation-ring units by the first filtration step.

The topology of a nonarchimedean local field is Hausdorff and totally disconnected because valuation balls are clopen. This file records those structures as named results, without registering additional global instances,…

Constructs the maps induced on valuation rings, residue fields, and residue units by a valued extension, with degree, trace, norm, and Frobenius results.

Restricts field automorphisms to residue-field automorphisms and identifies the resulting kernels and stabilizers with inertia subgroups.

Constructs the quotient of valuation-ring units by first principal units and identifies it, multiplicatively and additively, with the residue-field units.

This file supplies the local-field calculation used when the abstract class-formation framework is specialized to separable-closure units. All ramification and residue degrees below are the actual invariants of the valua…

This file records the valuation and topology on the Type 0 representative of an arbitrary-universe nonarchimedean local field.

The integer ring injects into the sequence of its finite quotients by powers of the maximal ideal. Its fraction field is therefore also small enough to be represented in Type 0. No countability of the field itself is ass…

An open finite-index subgroup of a nonarchimedean local field multiplicative group contains a standard subgroup built from a uniformizer and a sufficiently deep principal-unit group.

For a nonarchimedean local field, quotienting the field-unit group by the standard subgroup generated by a normalized uniformizer and U^n is canonically equivalent to quotienting the integer-unit group by U^n.

This module identifies the image of valuation-ring units in the field unit group with the valuation-one sphere and records that this subgroup is open in the native topology of a nonarchimedean local field.

The arithmetic Frobenius is first defined as finite-field Frobenius on the residue extension, then lifted to Gal(L / K) through the canonical residue-action isomorphism for a finite unramified extension.

Relates membership in the valuation ring to the ambient valuation and exposes the associated surjective multiplicative valuation with a uniformizer.

Builds the normalized valuation map Kˣ → ℤ and proves exactness of the sequence from valuation-ring units through field units to ℤ.

Records when the valuation ring of an extension field is integral over the base valuation ring, the hypothesis needed to restrict field norms integrally.

This file records the topology bridge used when a nonarchimedean norm is turned into a ValuativeRel: the topology already carried by a nontrivially valued field is the valuative topology for that induced relation.

This file provides the common algebraic norm map on unit groups. It is independent of any valuation or local-field structure, so valued-field and discrete-valuation APIs can share the same definition.

This aggregate exposes padic local-field structures, cyclotomic extensions, Teichmuller characters and reduction, and principal-unit comparisons.

A nonzero closed additive subgroup of ℤ[p] contains a nonzero principal ideal. Since every nonzero ideal of ℤ[p] is generated by a power of p, such a subgroup is open.

A continuous family on a compact space can be multiplied by one power of p so that every value lies in the actual p-adic integer ring.

This aggregate exposes the totally ramified and unramified cyclotomic modules.

Eisenstein generators, integral closures, uniformizers, and ramification indices for the p-power cyclotomic tower.

For a primitive p ^ m-th root of unity ζ, with m > 0, the local cyclotomic calculation proves that ℚp / ℚ[p] is totally ramified of degree φ (p ^ m), identifies its Galois group with (ZMod (p ^ m))ˣ, identifies its valua…

This file extracts the unit relation p · u = (ζ - 1)^φ from the translated Eisenstein polynomial.

This file packages the actual integral-closure complete-DVF model as a totally ramified extension.

This file identifies ℤ[p][ζ] with the actual integral closure and proves that it is a discrete valuation ring.

This file records that translating ζ by one preserves the explicit integral closure.

This file proves directly from its norm that 1 - ζ is prime in the explicit DVR ℤ[p][ζ].

This file maps the Eisenstein unit relation into the target valuation ring and proves e = [L : ℚ[p]], together with the uniformizer statement.

This file constructs the concrete equivalence from ℤ[p][ζ - 1] to the actual valuation subring.

This aggregate exposes arithmetic Frobenius for the unramified cyclotomic construction.

Let K be a complete discretely valued field with finite residue field k = Fq, let ζ be a primitive n-th root of unity, and suppose that n is prime to the residue characteristic. the unramified cyclotomic theorem states t…

The action on the p-th roots of unity lifts by Teichmüller representatives to p-adic units. It recovers the action on every p-power root present in the extension, without assuming that all p-power roots are present.

The two characters on a cyclotomic extension and its base change agree along the actual restriction homomorphism. Normality of the lower cyclotomic extension supplies the restriction; no bijectivity or compatibility of c…

This file connects Mathlib's normed and valuative structures on ℚp to the topology-first local-field interface used by this library.

Two units modulo a positive power of p annihilated by the same exponent coprime to p are equal if their reductions modulo p agree. The proof uses uniqueness of a simple polynomial root in a local ring.

A primitive p-th root in a domain defines a p-adic character of its algebra automorphisms over any base ring. Its reduction records the actual action on that root. Restricting scalars preserves this character because it…

This file identifies the standard p-adic integer and complete-DVF models, computes their principal-unit quotients, and records the logarithm/exponential power formulas used by local cyclotomic norm calculations.

Reduction from the p-adic integers through a positive prime-power quotient agrees with their residue map to ZMod p.

The actual p-adic integers, with their metric topology, are the ring of compatible residues. Reduction gives the forward map. Its inverse is constructed by the universal property of the p-adic completion, and is continuo…

Hensel lifting in the concrete complete discrete valuation field ℚ[p] gives a multiplicative section of reduction to (ZMod p)ˣ. Its values are (p - 1)-st roots of unity, including when p = 2.

A unit modulo a positive power of p whose (p - 1)-st power is one is the reduction of the Teichmüller representative of its residue.

This file constructs the reusable topological decomposition of ℤ[p]ˣ into its finite factor and its principal p-adic factor.

Finite and algebraic unramified extensions, their residue extensions, maximal unramified subextensions, and base change.

Let L and K' be intermediate fields of a common algebraic ambient field Ω. Starting from the primitive integral model of a finite unramified extension L/K, this file maps its generator and polynomial to the actual compos…

This file proves the polynomial core of the unramified base-change argument. A primitive integral generator whose monic model has separable reduction gives a finite unramified extension. The proof takes the actual integr…

The first finite step in the unramified base-change theorem is forced already by the finite unramified-extension definition and the fundamental inequality of the fundamental inequality. The actual quotient of value group…

The finite case of stability under finite composita says that the composite of two finite unramified extensions is again unramified. The proof first applies the unramified base-change theorem to one extension along the o…

Finite unramified valued extensions are expressed directly by the degree equality and residue separability condition.

The maximal unramified subextension is defined as a compositum. Compactness of a simple intermediate field and stability under finite composita imply that every one of its elements already belongs to a single finite unra…

The base-change proof uses the following exact Hensel step. If a monic polynomial over a Henselian valuation ring is irreducible over the fraction field and its reduction is separable, then that reduction is already irre…

The proof of the unramified base-change theorem applies Hensel's lemma after base change from K to an algebraic extension K'. This file supplies the source used there: the unique extension of a Henselian valuation to an…

Finite support in the compositum reduces the value-group equality and the forward residue-field inclusion to the corresponding finite statements.

Let L/K be an algebraic valued extension. Its maximal unramified subextension is the compositum, inside L, of all unramified subextensions. Since the finite unramified-extension definition defines an arbitrary unramified…

The generic tower and embedding-monotonicity lemmas extracted from the tame adapter.

For the maximal unramified subextension T, the maximal-residue theorem identifies the residue field with the separable closure of the base residue field and the value group with that of the base. This file proves the two…

The reverse residue-field inclusion in the maximal-residue theorem is the Hensel step from the residue-lifting argument: lift the minimal polynomial of a separable ambient residue element, then lift its simple linear fac…

A finite unramified extension of a Henselian valued field is separable. The proof follows the primitive-residue-element argument on p. 153: lift a primitive generator of the separable residue extension, use the fundament…

Canonical aggregate generated by the reviewed rehome.

The paragraph following the decomposition and inertia subgroup definitions observes that the decomposition, inertia, and ramification groups are closed in the Krull topology, also for an infinite Galois extension. Each f…

This file specializes mathlib's Dedekind-domain different ideal to complete DVF valuation rings. The ideal itself remains mathlib's differentIdeal; the extra API here connects it to the chosen valuation rings, the codiff…

Generic order-theoretic infrastructure for extending a natural-number-indexed subgroup filtration to the real line by the natural-number ceiling.

This file develops the decomposition and inertia subgroups of an absolute Galois group after the finite-level valuation-restriction layer.

Aggregate for the RamificationTheory.GaloisValuation.AbsoluteGalois folder.

Provides the public declarations in the RamificationTheory.GaloisValuation.AbsoluteGalois.FiniteExtensionCorrespondence Lean module.

This file isolates the valuation-restriction and separable-power lemmas used to pass from absolute Galois questions to finite intermediate fields.

Provides the public declarations in the RamificationTheory.GaloisValuation.AbsoluteGalois.InfiniteGaloisCorrespondence Lean module.

Focused aggregate for absolute Galois and ramification data of valued fields.

This module packages the closed subgroup attached to an intermediate field in the Krull topology.

An automorphism of a field generated by two normal intermediate fields is determined by its restrictions to those fields.

At each finite Galois level, this file uses the chosen integral-closure valuation from FiniteGaloisLevel and intersects the inverse images of its ramification groups. Independence from the chosen complete-DVF realization…

This module packages the canonical restriction map between two intermediate fields in a common ambient extension without requiring callers to install the auxiliary algebra and scalar-tower instances.

This file provides the group-theoretic lower ramification APIs used by local CFT. Concrete valued extensions supply the action quotient estimates; the subgroup and normality/antitonicity consequences are proved here.

This module owns the opaque quotient carriers of a lower ramification filtration and their construction, elimination, lifting, and mapping API. Arithmetic Herbrand functions and valuation-action specializations live in R…

Public root for the finite-group foundations of the real Herbrand function, subgroup and quotient filtrations, and quotient-fibre averaging.

This file formalizes the remaining finite-group calculation in the Herbrand quotient theorem. For a normal subgroup H, the depth on G defines the lower filtration Hs = {τ : H | s + 1 ≤ depth τ}. For a nonidentity class i…

This file supplies the group-theoretic content of the Herbrand-function sum formula. The old AntitoneNormalSubgroupFiltration.herbrandStep starts with |G₀| / |G₀|; the normalized Herbrand function has, on (m,m+1), slope…

This file contains the completion-free finite-group bookkeeping used in the Herbrand quotient theorem and the quotient and tower filtration theorems. It packages the filtrations induced on a subgroup and on its quotient…

This file isolates the part of the Herbrand quotient theorem which is independent of valuations. A discrete nonarchimedean depth has the two properties of i(σ) = v(σ(a) - a) used in the ramification-depth proof: multipli…

For a possibly infinite Galois extension L/K, the Galois group acts transitively on the extensions to L of a nontrivial absolute value of K.

Over a Henselian base of residue characteristic zero containing all p-power roots, finite p-group inertia yields central restrictions at larger finite layers and a nonidentity central element of the absolute Galois group…

Every field element lies in its actual finite Galois normal closure. Pullback restricts inertia to that layer, and the comap valuation subring has residue characteristic zero. Finite inertia is commutative there, and the…

For a possibly infinite Galois extension, this file constructs the canonical isomorphism between the decomposition group of an exact absolute value and the Galois group of the localization over the completed base field.…

The algebraic localization comparison is algebraically a MulEquiv. This file establishes its finite-support continuity input: fixing one element of the algebraic localization only requires fixing finitely many elements o…

For an actual inertia element, ramification can be tested after restriction to every finite Galois intermediate field. A failure of the defining principal-unit condition involves one unit, which already lies in one such…

Restriction to a finite Galois layer lands in that layer's actual ramification group. Its finite image is therefore a p-group in residue characteristic p. The kernels of these continuous restrictions form a Krull neighbo…

This file proves functoriality of the decomposition, inertia, and ramification groups under a commutative square of field embeddings. Only normality of the lower extension is needed to restrict conjugation to its Galois…

The canonical finite tame character is the raw uniformizer character raised to e / n. The raw tower exponent is the relative ramification index. The following arithmetic converts that exponent into the ratio of the actua…

This file contains the exactness and quotient consequences of the character constructed in CharacterMap. It is the exactness part of the inertia-character exact sequence that does not require the finite-cardinality surje…

This file records the source lemmas for the canonical map Iw -> Hom(Delta / Gamma, lambda) in prime-decomposition theory. We do not package the final value-group quotient here. Instead, we prove the pieces which make the…

For a finite separable extension of complete discretely valued fields, the extension of the base valuation is unique. Consequently every base-field automorphism stabilizes the chosen target valuation ring and the full Ga…

This file records the functorial conjugation law for chosen valuations: inside a fixed Galois extension, conjugating the chosen valuation subring conjugates the decomposition group. The inertia and ramification parts req…

An inertia group is bounded by the degree of its Galois extension. An embedding into a concrete cyclotomic field therefore bounds its cardinality by Euler's totient.

Identifies both ideal ramification-index conventions with the additive valuation of a mapped base uniformizer for an injective map of discrete valuation rings.

Factors a mapped uniformizer into a target uniformizer power and a unit, with exponent given by its additive valuation. For a local DVR algebra, the exponent is the ramification index.

The decomposition field is the fixed field of the decomposition group. This formulation uses absolute values and therefore includes the archimedean case.

This file starts with clause (i): the restriction of w to its decomposition field has a unique extension back to L. The proof works for finite or infinite Galois extensions and for archimedean or nonarchimedean valuation…

This file identifies the decomposition field with the literal intersection L ∩ Kv inside the algebraic localization Lw. It then records the canonical residue-field isomorphism and equality of absolute-value ranges in the…

This file gives the three tower-intersection formulas in their common ambient Galois group. The decomposition-group statement is formulated for arbitrary absolute values, including the archimedean case. The inertia and r…

This aggregate exposes prime contractions, decomposition and fixed fields, conjugation, orbit cardinalities, and valued Galois comparisons in Dedekind extensions.

This file manages the Dedekind-domain part of Hilbert ramification theory in prime-decomposition theory. The implementation uses mathlib's ramification/inertia theorems where those are already the source proof, but the d…

This file contains reusable criteria for proving that a prime in a number field compositum is unramified from the inertia groups of its two factors.

This file records the conjugation statement in prime-decomposition theory: the decomposition group of a conjugate prime ideal is the conjugate subgroup.

This file contains the group-theoretic fixed-field part of the tower ZP ⊆ TP ⊆ L in prime-decomposition theory.

This file records the ramification-theoretic step in the proof of the global Kronecker--Weber theorem. If a subgroup of a finite Galois group contains the inertia group at every prime of the top field, then its fixed fie…

This file contains the fixed-field layer of prime-decomposition theory. The Dedekind-domain file defines the decomposition and inertia groups attached to a prime ideal; here we view those groups as subgroups of a finite…

This file proves the ramification and inertia invariant statements for the contracted primes PZ and PT appearing in the decomposition and inertia fixed-field tower.

This file records the parts of the prime-decomposition tower identity that are already available from the Dedekind-domain Galois action and mathlib's ramification/inertia API.

This file specializes the fixed fields ZP and TP to rings of integers of number fields and defines the contracted primes p, PZ, and PT.

This file records the tower identities for ramification indices and inertia degrees used in the prime-decomposition tower identity.

The ideal-theoretic inertia group has cardinality equal to the canonical ramification index of a finite separable extension of complete discrete valuation fields.

For a Henselian discrete valuation field of residue characteristic zero containing all p-power roots, a Kummer extension supplies nontrivial inertia and hence a nonidentity element of the absolute Galois center.

For a valuation ring with finite decomposition group, a compatible surjective ring map acting by principal-unit multipliers gives a field automorphism of p-power order in positive residue characteristic p. In residue cha…

For a complete discretely valued field K and a finite Galois intermediate field E of an algebraic closure, an existence theorem for the integral closure of the valuation ring of K supplies complete-DVF structures on E. T…

The ramification filtration of a finite extension depends only on its valuation ring. For a finite Galois level over a complete discretely valued field, uniqueness of the extended valuation therefore identifies the filtr…

The residue extension need not be separable. Its automorphism group has order its separable degree. Cancelling this factor from the actual decomposition identity gives |I| = e finsep, which is the cardinal input for Stac…

Roots of unity in the base force trivial residue action on those roots. For a finite extension with Henselian valuation ring and residue characteristic zero, the corresponding finite-order inertia elements commute with d…

The faithful residue-unit character in characteristic zero turns a nonidentity prime-order inertia element into an actual primitive root in the residue field.

Define finite inertia restriction and transition maps, compare them with Galois restriction, and prove compatibility and surjectivity over a Henselian base.

The actual residue-unit character has ramification kernel. Finite inertia fixes values, so this character is defined on all inertia. In residue characteristic zero its kernel is trivial and inertia is commutative. In res…

A finite-order decomposition element fixes the original valuation's values. Consequently every finite inertia element lies in the value-trivial subgroup.

In positive residue characteristic p, factoring a finite annihilating order as p^a times a prime-to-p integer reduces the assertion to prime-to-residue torsion triviality. In residue characteristic zero, every positive f…

Proves injectivity of exponential-characteristic-power maps on field units and surjectivity on finite subgroups. Scaling a character by such a power preserves its kernel and, for a finite source group, its range.

Identifies a finite subgroup of field units with all roots of unity of its order and produces a primitive root. Finite characters are then expressed as surjections onto these root groups with the corresponding kernel quo…

The DVF filtration uses units of the valuation ring, whereas Hilbert's ramification group uses the principal-unit subgroup of the field units. This file identifies their first levels before comparing group actions.

This file records the fixed-field maximality statements behind the inertia-field maximality theorem and the ramification-field maximality theorem. The valuation-theoretic words "unramified" and "tamely ramified" still re…

For M = L ^ H, this file works with the literal restricted valuation ring OM = OL ∩ M. The ramification number of an actual element of Gal(M/K) is the value of the principal ideal generated by all of its integral displac…

For M = L ^ H, this file defines e(L/M) from the literal inclusion OM = OL ∩ M → OL. The definition and its comparison with the zeroth depth subgroup require no completeness or Henselian hypothesis.

For a normal subgroup of a finite Galois group, this file uses the literal fixed field and the restriction of the chosen top valuation ring. Unique extension identifies that restricted ring with the integral closure of t…

In a finite Galois extension, if every automorphism fixing b also fixes a, then the simple field generated by a is contained in the simple field generated by b.

The finite ramification subgroup is the Sylow subgroup of finite inertia for the residue characteristic. Surjectivity of actual inertia restriction gives compatible finite ramification lifts. Compactness then supplies an…

Henselianity identifies the selected extension valuation ring with the integral closure, so every base-field automorphism preserves it. Consequently the fixed integers in the residue exact sequence over an intermediate f…

A lift of an inertial automorphism fixes the actual residue scalars from the intermediate field. The scalar-image comparison turns its residue action into an automorphism over the base of the decomposition residue exact…

The defining principal-unit condition for ramification is preserved by conjugation by every decomposition automorphism. Over a Henselian base, decomposition is the full automorphism group, so both actual inertia and actu…

Over a Henselian base the actual inertia restriction is surjective. If upper inertia is finite, ramification at both levels is the unique Sylow subgroup for the residue characteristic. A surjective homomorphism carries a…

Reduction acts on the actual residue-field algebra. Fixed integers descend to the base field, identifying the scalars needed for residue surjectivity. Finite residue bases lift to finitely many algebraic field elements,…

Trivial residue action remains trivial on an intermediate Galois extension through the canonical residue-field maps of the chosen valuations.

The residue field of the fixed integer ring and the actual residue field of an intermediate field have the same image in the selected residue field. The comparison is proved on integer representatives. It does not assume…

This file attaches the group-theoretic Herbrand functions directly to the real lower ramification groups of RealLowerGroups. The only valued-field input is the stated unique-extension hypothesis that the chosen valuation…

This leaf contains the completion-free endpoints of the Herbrand quotient theorem and the quotient and tower filtration theorems. The private lemmas below isolate the finite-group averaging argument used in the quotient-…

Relate the residue-unit inertia character to decomposition and residue actions. Finite inertia characters are injective in residue characteristic zero.

For a finite Galois extension of complete discrete valuation fields, the decomposition-side inertia subgroup has cardinality equal to the canonical ramification index.

This is the finite-cardinality consequence of the inertia-subgroup cardinality formula used when the base completion is identified with a concrete local field.

In residue characteristic zero, inertia fixes every root of unity. Each root is a valuation-ring unit. Its image under inertia has the same reduction, so the injectivity of Henselian root reduction identifies the two roo…

A selected valuation above a prime-degree Galois extension with unchanged residue field yields a nontrivial finite inertia p-group.

Computes powers of the local tame character on conjugate inertia elements using the root-group map induced by the residue-field action.

Proves that the local tame character group map is surjective and that its kernel is the principal-unit inertia subgroup.

Defines group objects for local inertia and the roots of unity of the tame order. It presents the finite local tame character as a homomorphism between them.

Defines power homomorphisms on the local tame root group and proves injectivity for exponential- characteristic powers. These maps are surjective when the acting group is finite.

For an infinite algebraic extension, the canonical Lw is the algebraic localization L Kv, not the whole metric completion. This file records the density consequences needed to transport inertia and ramification condition…

This file packages the decomposition-group equivalence of the localization and decomposition comparison as equivalences of the valuation-subring decomposition, inertia, and ramification groups. The difficult global-to-lo…

This file proves the algebraic, noncomplete form of the monogeneity argument used in the monogenic integral-generator theorem. The proof uses the finite integral closure supplied by unique extension, a primitive residue…

This file proves the orbit-polynomial ideal identity before normalization of the fixed-field valuation. It uses the literal fixed field and its literal restricted valuation ring; no completeness or Henselian hypothesis o…

This file collects the reusable algebra, finiteness, Galois, and nonarchimedean facts needed to compare a global algebraic localization with an extension of ℚ[p].

This file contains the generic polynomial congruence lemma used by the completion-free formalization of ramification-number theory.

The intrinsic ring predicate used by the DVR character kernel is equivalent to the field-unit predicate used by Hilbert ramification. The proof constructs the required units and uses the valuation alternative, without an…

Proves that the principal-unit multiplier condition is preserved, in both directions, by a local-ring equivalence intertwining the ring maps.

The principal-unit condition forces trivial residue action, so the ramification group inside inertia has a canonical image in the decomposition group.

This file contains the fixed-field part of the ramification-field definition, over the decomposition field Zw. The base valuation-subring file owns the definitions of Gw, Iw, Rw, Zw, Tw, and Vw; here we record the tower-…

This file records the first structural facts about the classical ramification subgroup Rw. The key point for the later character map Iw -> Hom(Delta/Gamma, lambda) is that Rw is a normal subgroup of Iw, not merely a subg…

This file gives the noncomplete version of the ramification number used in ramification-number theory. Under the stated unique-extension and separable-residue hypotheses, the monogenic integral-generator theorem supplies…

This is the field-facing, noncomplete form of the Herbrand-function sum formula. The monogenic integral-generator theorem supplies the generator hidden inside intrinsicRamificationNumberOfUniqueExtension; the public endp…

The public endpoint has no generator argument. The monogenic integral-generator theorem supplies the top integral generator internally, while the fixed-field ramification number is the intrinsic value of its displacement…

A ramification automorphism whose order is nonzero in the residue field is trivial. For a moved element, divide its successive conjugate differences by the first nonzero difference. Ramification makes every resulting quo…

This file gives the intrinsic definitions and the elementary structural facts in the real lower-ramification definition and the lower-ramification base-change law. It uses discretely valued fields, not complete discretel…

For a (possibly infinite) Galois extension and a chosen extension valuation, the residue extension over the decomposition field is normal and reduction gives the exact sequence 1 → Iw → Gw → Gal(λ/κ) → 1. The base residu…

For a chosen valuation on a Galois extension, every automorphism of its residue field over the residue field of the decomposition field lifts to an ambient Galois automorphism stabilizing the chosen valuation. This is th…

Transports the uniformizer-ratio tower identity to a common field where the upper action fixes the coefficient map. This removes the unit correction and gives the relation at the additive valuation of the mapped uniformi…

Defines the tame order as the size of the inertia-character image and constructs a surjective character onto all roots of unity of that order. It identifies the principal-unit kernel and produces a primitive root in the…

This consumer uses the native decomposition action on the actual valuation subring. Both individual ring maps in the sparse comparison are supplied by that action; their coefficient compatibility is definitional.

The coefficient in π c = s(π) is constructed from the ring map and the element. Existence and nonzero-factor cancellation identify it with any actual unit ratio, without using a ramification character.

Proves that the cardinality of inertia is the tame image order multiplied by the cardinality of principal-unit inertia.

This owner starts from the actual ideal inertia of a group acting on a DVR. It constructs the uniformizer-ratio unit inside the ring and then reduces it. No ambient fraction field, scalar tower, chosen value group, or su…

Proves normality of maximal-ideal inertia and computes the conjugation of uniformizer-ratio units. The residue character intertwines group conjugation with the induced residue-field action.

Proves that fixing a unit times a uniformizer power makes the same power of the inertia character trivial. It deduces the corresponding result using the additive valuation of a nonzero fixed element.

Characterizes triviality of the DVR inertia character by principal-unit multipliers on all ring elements. It defines the corresponding inertia subgroup and identifies it with the character kernel.

Expresses membership in principal-unit inertia by requiring each multiplier minus one to lie in the maximal ideal.

The ring predicate is first put in actual ideal inertia. The native Hilbert predicate comparison then supplies the ramification element and its p-power order. The final ring-kernel scope consumes this proved order statem…

Proves ratio and residue-coefficient identities for compatible ring maps and group actions across a DVR tower. The exponents are identified with the additive valuation and ramification index of a mapped uniformizer.

Computes powers of the tame character using any uniformizer and proves their compatibility with conjugation and the residue-field action.

Proves that the finite tame order is invertible in the residue field and divides the valuation of every nonzero fixed element. It consequently divides the ramification index of an injective DVR algebra with a compatible…

Proves that the tame order divides the length-based order of vanishing of every nonzero fixed element in a discrete valuation ring.

The first isomorphism theorem identifies the actual residue-character image with inertia modulo the same principal-unit wild subgroup.

Extracts a ring coefficient from the uniformizer-ratio unit, together with its unit property and the equation relating a uniformizer to its image under the action.

Proves that a field embedding induces a bijection on n-th roots of unity for nonzero n when the source contains a primitive n-th root. It also bundles root groups and their maps induced by coefficient homomorphisms.

Finite Galois restrictions of each positive closed derived term land in finite p-group commutators. The Krull neighborhood basis therefore supplies an open-normal p-group basis on the derived term itself.

The algebraic residue extension is purely inseparable, so its Galois action is trivial. On each finite Galois layer the inertia character sends the commutator to one, placing it in the actual wild ramification group.

The two inertia-cardinality formulas and the actual tame-degree divisibility show that the ratio of the ramification index to the tame degree divides the wild order. Thus it is a residue-characteristic power, and is prim…

This file constructs the graded uniformizer homomorphism under the standing hypotheses of ramification-number theory. Completeness is not assumed. The injectivity statement includes the necessary separability hypothesis…

This file supplies the noncomplete integral-closure input used in ramification-number theory. For a finite Galois extension with a uniquely chosen extension of the base discrete valuation, the Galois orbit polynomial of…

An algebra equivalence transports the ambient copy of valuation-subring inertia to the corresponding ambient inertia subgroup for the pulled-back valuation subring.

For a finite Galois extension with a uniquely extended discrete valuation, suppose b is closer to an integral element a than any nontrivial automorphic displacement of a. Then every automorphism fixing b also fixes a. Th…

For a normal field tower M / L / K with uniquely extended discrete valuations, the valuation-ring action of an automorphism of M / K on an element coming from L is the image of the valuation-ring action of its restrictio…

This file manages the ordinary valuation-subring decomposition/inertia exact sequence. For an arbitrary valuation subring the residue action need not be onto the full residue automorphism group; the canonical theorem is…

The global Kronecker--Weber proof generates the full Galois group by the inertia groups at the finitely many ramified primes. Since the group is abelian, the cardinality of the subgroup that they generate is at most the…

Public aggregate for the intrinsic local ramification filtration and its base-change and unramified specializations.

The target field can carry two algebra structures whose base fields are identified by a valuation-preserving field equivalence. This file proves that the resulting Galois groups have the same upper filtration, after iden…

The actual finite-level upper filtration attached to the canonical complete-DVF structure of a nonarchimedean local field, together with its right-limit subgroup and the intrinsic predicate for an upper jump.

The canonical complete-DVF valuation on a finite local extension specializes the general comparison between the first lower group and Hilbert's ramification group. The latter is transported from the decomposition group b…

The residue field of a nonarchimedean local field is finite. A finite extension of its chosen complete discrete valuation has finite-dimensional residue field, hence a separable residue extension. This supplies the resid…

This file connects the concrete unramified-valued-extension predicate with the actual upper ramification groups of a finite local extension.

The finite invariant-ring API proves that a prime residue extension is normal. The residue-action exact sequence also needs the corresponding profinite statement. The proof is the same finite-orbit argument as in this co…

This module compares the exponential-valuation presentation of ramification with the canonical complete-DVF presentation. The comparison is independent of any cyclotomic or Kronecker--Weber hypotheses.

Public aggregate for existence, uniqueness, norm formulas, and ramification properties of absolute values on algebraic field extensions.

A nontrivial real-valued absolute value on a complete field extends uniquely to every algebraic field extension. Both the archimedean and nonarchimedean branches are included.

The nonarchimedean branch uses mathlib's spectral norm. The archimedean branch uses the completed Ostrowski theorem, reducing the statement to the standard ℝ and ℂ absolute values.

Algebraic facts about the finite norm formula used in the explicit proof of The algebraic-extension norm formula, together with restriction of a valued field tower to an intermediate field.

The factorization form of Hensel's lemma makes the closed unit ball of the finite norm-formula value equal to the integral elements over the base valuation ring. This supplies the strong triangle inequality and hence the…

This file reuses the algebraic normalization and irreducibility obstruction from the irreducible-polynomial coefficient bounds. The factor lift is supplied directly by the factorization form of Hensel's lemma in the prim…

This file packages the explicit algebraic-extension statement. A valuation is represented by its valuation subring, so uniqueness is literal equality of valuation subrings (equivalently, equivalence of valuations).

The factorization form of Hensel's lemma forces the endpoint coefficient estimate for every irreducible polynomial. Applied to the norm-formula value, this says that every algebraic element or its inverse is integral ove…

The first part follows the proof on pp. 149--150: residue-basis lifts are multiplied by representatives of distinct value-group cosets, and the resulting family is linearly independent over the base field. The second par…

The nonarchimedean valuation construction supplies the irreducible coefficient estimate. The unique nonarchimedean extension to a splitting field is invariant under all ground-field automorphisms. Normality of a splittin…

Once the actual integral closure of a valuation subring satisfies the valuative dichotomy, it is contained in every extension valuation ring. Its integrality over the base then forces the center of every such overring to…

For an exact extension wL of an absolute value vK, this file constructs the compositum of L and the completed base field inside wL.Completion. The construction applies to arbitrary algebraic extensions and does not use a…

Provides the public declarations in the ValuationTheory.AbsoluteValue Lean module.

This file keeps only the lightweight explicit definitions used by the current Section 4 formalization. The old experimental completion and norm formula development was removed because it duplicated mathlib APIs and no lo…

This file supplies the canonical absolute value, completion maps, density, and complete-target universal property for real-valued absolute values. An extension is expressed directly by AbsoluteValue.Extends; no extra con…

The localization arguments of the ramification-localization construction are naturally multiplicative, whereas the unramified predicates of the unramified-extension construction use additive exponential valuations. This…

A reusable predicate for exact extension along an algebra map.

The strong triangle inequality is equivalent to boundedness on natural numbers for real-valued absolute values.

A complete field with an archimedean real-valued absolute value is isomorphic to ℝ or ℂ, with the absolute value obtained from the standard norm by a positive exponent at most one.

For a complete nonarchimedean absolute value, a nonzero element of the open unit ball generates a separated and precomplete principal filtration on the closed unit ball. These facts are shared by the coefficientwise Hens…

The spectral norm gives the unique extension of a complete nonarchimedean absolute value to an algebraic field extension.

This module collects the valuation-theory material used by local class field theory. General results on equivalence of absolute values, Ostrowski theory, approximation, and rational-function examples are imported from Ma…

This aggregate exposes the core absolute-value structures, their comparison theorems, and exponential valuations.

Provides the public declarations in the ValuationTheory.AbsoluteValue.Theory Lean module.

This file develops additive valuations with values in WithTop ℝ, their equivalence under positive scaling, and the associated absolute values and valuation rings. For discrete valuations it describes prime elements and t…

This file records the valuation ring attached directly to a multiplicative absolute value in the nonarchimedean case. It is the section-3 object used by the finite-degree norm construction before any discrete-valuation-f…

Canonical aggregate generated by the reviewed rehome.

If a natural exponent below p^(s+1) differs from one, its difference from one is nonzero and has p-adic order below s+1. The absolute value of that integer is strictly below the modulus, so divisibility by the modulus is…

The residue-field characteristic of a valuation subring is preserved by pullback along a field embedding. The proof compares natural-number casts with membership in the nonunits.

A field embedding preserves the nonunit condition for the pulled-back valuation subring. Consequently equality of integer residues downstairs implies equality upstairs, so residue characteristic zero descends. No algebra…

The setup uses nontrivial real-valued absolute values throughout. For an absolute value v on K, we use mathlib's completion v.Completion and its concrete algebraic closure. The absolute value bar v on that algebraic clos…

Public root for factorization, scalar extension, finite products, norm, and trace. This module is upstream of local-field and local class field theory.

In characteristic p, the local Artin–Schreier images are open. The diagonal density from weak approximation therefore realizes any finite collection of local additive Artin–Schreier classes by a global field element.

If L/K has power basis generated by α, then the scalar extension A ⊗[K] L is canonically A[X]/(minpolyK(α)). The equivalence below is the canonical algebra equivalence used in scalar-extension decompositions.

Norm and trace formulas compare multiplication by an element of L before and after extending scalars from K to Kv. These lemmas state that comparison directly for the canonical element 1 ⊗ₜ x.

For every exact extension w | v, multiplication in Lw gives the map Kv ⊗K L → Lw. Taking all components produces the canonical map which occurs in the tensor-product decomposition over a completion. This construction is…

The completion of a finite extension is generated by the original field. The canonical completion algebra preserves cyclotomic extensions.

The descended intermediate field receives the discrete valuation of its localized integral closure. The two actual tensor maps identify its completion with the prescribed extension, preserving both embeddings.

Powers of a ground-field uniformizer are cofinal in the target valuation balls. The Archimedean property is used only for the actual value group of the target valuation, which is order-isomorphic to the multiplicative in…

A generator separable over the original field gives a finite separable intermediate field. Its scalar extension maps onto the given extension of the completion, and the equality of degrees makes this actual map injective…

The original valuation supplies a norm with the same uniformity on WithVal. Its completion is therefore the given valuation completion. Density of the canonical ground-field map then descends finite separable generators.

The image of a finite extension is contained in the field generated by the images of a finite linear basis. Those images remain integral after extending the scalars to the completion. Neither Henselianity nor separabilit…

The actual tensor map onto an extension completion makes a homomorphism over the base completion determined by its values on the original field.

Scalar extension of the original homomorphism, transported through the actual tensor comparison, gives a homomorphism over the base completion. Only the source extension needs to be finite and separable.

The extension formula on original field elements and extensionality over the base completion imply preservation of identities and composition.

A separable extension of the actual valuation completion is generated by any embedded separably closed extension of the original field. Each element lies in a finite simple extension whose descended generator is in that…

Multiplication of the two given embeddings is surjective because the embedded separably closed field generates the separable extension of the valuation completion. No Henselian hypothesis is used for surjectivity.

The map of completions supplies the scalar algebra. Multiplication then gives the actual tensor map to the completion of the extension field. Class-valued statements specify this algebra's scalar action explicitly, avoid…

The canonical decomposition of the completion tensor-product decomposition gives the sum of the local degrees and the product/sum formulas for norm and trace. Since the global norm and trace lie in K, their Lean statemen…

The tensor image of a finite extension is finite-dimensional over the complete base field, hence closed. If it contains a dense copy of the extension field, this image is the entire target ring.

A field isomorphism which carries one valuation to an equivalent valuation induces an isomorphism of the actual valued completions. The construction preserves the original embedding of the field.

The extended valuation has the same value group as the original valuation. For any discretely valued field, the native completeness of the valued completion therefore supplies a complete discrete valuation. The canonical…

A relative field automorphism carrying one prolongation to another induces a completion isomorphism commuting with the map from the completed base field.

For a simple finite extension L = K(α), the extensions of a nontrivial absolute value of K correspond to the distinct irreducible factors, over the completion, of an irreducible polynomial having α as a root. The final t…

For a finite separable extension L / K and a discrete nonarchimedean absolute value v on K, this file proves the exact degree formula ∑{w ∣ v} ew fw = [L : K]. The proof makes explicit the two facts used implicitly in th…

For a finite extension L / K, the localization L Kv inside the metric completion Lw is already all of Lw. The proof uses no separability: the image of Kv ⊗K L is finite-dimensional and closed, but contains the dense copy…

These algebraic lemmas are the finite-product linear algebra used in tensor-product norm and trace formulas. Mathlib has the binary trace formula and the determinant of a binary product map; the dependent finite-product…

Embed a finite separable extension into an algebraic closure of its base. The generator descended there belongs to the image of the extension, so it pulls back to a generator of the original field with the same degree.

Only finitely many coefficients from the algebraic extension occur in a tensor element. Adjoining those coefficients gives a finite intermediate field over which the element is already defined.

The tensor comparison gives the isomorphism on separable closures. The purely inseparable comparison with algebraic closures connects it to the actual Field.absoluteGaloisGroup, with its Krull topology, in every characte…

The correspondence of homomorphisms respects composition. Passing to units therefore gives a group isomorphism of automorphisms, whose action extends the original action on the finite separable extension.

The actual extension map is bijective: the original field is embedded in its completion, and separable elements descend uniquely to a Henselian target. The inverse correspondence retains the original field embeddings.

The normed model comes from the given discrete valuation. Its unit ball is isomorphic to the original Henselian valuation ring, so the normed completion theorem applies to the actual valuation completion.

The range of the actual tensor map is the field generated by the image of an algebraic intermediate field. For a finite separable intermediate field of a Henselian DVF, this identifies its own valuation completion with t…

The field generated over the completion by the image of an intermediate field has exactly the corresponding fixing subgroup. The equality is for the actual constructed automorphism correspondence, and holds without requi…

The image of a separable element under a homomorphism of completions is separable over the target field. Henselianity places that image in the original target field, producing a unique homomorphism before completion.

The coefficients of a monic divisor of a separable polynomial are separable over the original field. Separable algebraic closedness in the completion therefore descends the divisor, preserving monicity and divisibility.

A finite separable intermediate field has a primitive element. The open stabilizer of its image is sent into the subgroup fixing that intermediate field, proving continuity for the Krull topologies at the identity.

Tensor extension and restriction through the chosen embedding are inverse. The resulting group isomorphism retains the action on each embedded element. No continuity or comparison theorem is assumed.

The automorphism is transported from id ⊗ σ through the actual tensor comparison. Its values on the chosen separable closure determine it, so the resulting extension preserves composition.

The actual tensor map is injective because its source is a field, and surjective by descent of finite separable generators. In particular it applies to the usual lift between the two separable closures.

In a finite normal extension, the Henselian valuation is invariant under ground-field automorphisms. An element approximable by ground-field elements must therefore be fixed by every automorphism. Applying this to the sp…

Restriction is continuous. The source of restriction is the compact Galois group of a separable closure, and the target is Hausdorff, so its inverse is continuous as well. Both maps retain the chosen embedding.

Each tensor element comes from a finite subextension. Inverting a nonzero lift there and mapping the inverse back proves the field property without assuming a comparison map is injective.

The minimal polynomial of a primitive element remains irreducible over the actual valuation completion. The adjoined-root presentation of scalar extension therefore makes the tensor product a field.

the completion construction constructs localizations using the absolute-value completion v.Completion, whereas the local Kronecker--Weber local cyclotomic theorem is stated over mathlib's concrete field ℚ[p]. For the rat…

This is the algebraic core of tensor-product decompositions. A squarefree factorization of the base-changed primitive polynomial gives the canonical product of its simple factor algebras.

This file records the algebraic source lemma underlying the extension-factor correspondence. Multiplicities are deliberately discarded: extensions of a valuation correspond to the distinct irreducible factors over the co…

For an integer nonzero in the original field, every finite tuple of local multiplicative power classes is represented by a single global unit. Hensel's lemma supplies the open local power subgroups; weak approximation th…

An automorphism over the common base preserves an embedded separably closed separable extension. Restricting both the automorphism and its inverse gives an automorphism of that extension, compatible with the original emb…

An embedding from a separably closed field contains every element that is separable over the common base, without any algebraicity assumption on the ambient extension or on the separably closed field over that base.

The algebraic closure is purely inseparable over the separable closure, so an automorphism is uniquely determined by its restriction. Normality supplies extensions of automorphisms, and restriction is continuous for the…

Every element of the algebraic closure has an exponential-characteristic power in the separable closure. Stabilizers of those powers form finite intersections of open subgroups. Injectivity of Frobenius then controls the…

The roots of a factor of a separable ground-field polynomial belong to the relative separable closure. A monic factor therefore has its coefficients in that closure, even when the ambient field extension is not algebraic…

A nearby root supplied by polynomial approximation generates the same extension as the original separable element. Comparing the degrees also shows that the new generator is separable over the dense subfield, with the or…

A separable monic polynomial is the product of its distinct normalized irreducible factors, and those factors are pairwise coprime. These are the factorization facts used in the Chinese-remainder proof of tensor-product…

Approximate the minimal polynomial by a monic polynomial over the dense subfield. Continuity of roots produces a nearby root in the algebraic closure, and Krasner's lemma places the original generator in its adjoin.

Every relative automorphism preserving the valuation extends to the completion. If all automorphisms preserve the valuation class, comparison with the canonical surjective tensor map shows that the degree is unchanged an…

For a finite separable extension L / K, the canonical map L ⊗K Kv → ∏{w|v} Lw is an isomorphism. The proof follows the construction: choose a primitive element, factor its mapped minimal polynomial, apply the Chinese rem…

These are the purely linear-algebraic implications for a finite product decomposition. They deliberately state the product terms as the components of a supplied algebra equivalence. A tensor-product decomposition identif…

Weak approximation gives a dense diagonal embedding in a finite product of inequivalent valued fields, and hence in the product of their completions.

Scalar multiplication on WithVal v is multiplication by the image of the scalar. Its uniform continuity supplies the existing completion algebra over the original field, without choosing a topology on that field.

Equivalent valuations on a field have the same discrete rank-one property.

This file supplies general-purpose facts about Mathlib's normalized additive valuation on a discrete valuation ring which are independent of any chosen valued-field presentation.

This file contains small generic source lemmas used to pass from completeness for a positive power I ^ n back to completeness for I.

Focused aggregate for discrete valuation fields, extensions, completions, Henselian structures, integral closures, and residue fields.

An embedding into an ambient complete DVF can make a uniformizer easier to recognize. For a finite separable extension, uniqueness of the extended valuation transports that recognition back to the chosen valuation.

The extension is the actual AdjoinRoot of the irreducible reciprocal polynomial. Its standard power basis supplies the degree. The inverse root generates the same algebra, satisfies the Artin--Schreier equation, and supp…

The polynomial X ^ n + C π X ^ (n - 1) - C π is Eisenstein at a prime parameter π when 1 < n. In an integrally closed domain it remains irreducible over the fraction field. An inverse of any root satisfies α ^ n - α = π⁻…

The standard AdjoinRoot of the fraction-field Eisenstein polynomial already has its canonical coefficient-ring algebra. Its root is integral because it annihilates the displayed monic coefficient-ring polynomial. Compari…

The inverse of a prime uniformizer cannot equal x ^ n - x for n > 1: its reciprocal polynomial is Eisenstein and would otherwise have a root in the base field. The argument does not require Henselianity or a characterist…

In characteristic p, translating X ^ p - X by a root gives the full splitting of X ^ p - X - C a. This source is purely algebraic and places no irreducibility, degree, normality, or valuation hypothesis on the field.

The field-norm valuation restricts to the degree-th power of the base valuation. After integer normalization, multiplying a nonzero extension-field element by a suitable inverse uniformizer power makes its value exponent…

Choose a prime uniformizer in the actual base valuation ring and construct the Artin--Schreier extension from its reciprocal Eisenstein polynomial. The localized integral closure supplies an actual extension valuation. T…

This is the basic one-dimensional API for fields equipped with a chosen rank-one discrete valuation.

In mixed characteristic, a bounded exponent different from one gives a coefficient (1-a)/p^(s+1) of value strictly greater than one. The numerator has smaller p-adic order than the denominator. No completeness, discreten…

Mathlib has the predicate Valuation.HasExtension and the induced valuation subring/residue-field API. This file proves the field-extension form of Chevalley's valuation extension theorem from mathlib's maximal local subr…

This file formalizes the recursive coefficient construction in the recursive coefficient proof. Given a section of the residue map and a uniformizer π, every element of the valuation ring has uniquely determined successi…

The actual common-top part of Abhyankar's lemma needs valuation data on the compositum L ⊔ K' inside a common ambient field. This file records the purely field-theoretic source facts before any valuation extension is add…

The exponent of an automorphism on a primitive p-power root reduces to its exponent on any primitive p-th root in the same field. The two roots need not be chosen compatibly.

Restricting an automorphism along two field towers preserves its exponent on primitive roots. The primitive roots in the two fields may be chosen independently; neither bijectivity of restriction nor a compositum hypothe…

An automorphism fixing the lower cyclotomic field commutes with an automorphism fixing the other normal field. A primitive root in the lower field generates the upper cyclotomic extension, so their commutation on the two…

A common primitive root proves that the upper cyclotomic field is generated over the lower cyclotomic field by the other field's image. Coprime degrees then give the original prime degree after this base extension.

The action on a primitive root embeds the automorphism group into the units of ZMod p. The primitive root and its generating property come from the cyclotomic extension itself; no irreducibility assumption is needed.

A primitive root in the given closure generates an actual cyclotomic intermediate field. The characteristic only needs to avoid the root order.

The normalized valuation and its uniformizer are constructed from the original valuation ring. Thus the norm obstruction needs only the Henselian discrete valuation and residue characteristic two.

Over a discrete valuation ring, an integral power basis with Eisenstein minimal polynomial generates every integral element of its fraction-field extension. Clearing polynomial denominators gives a uniformizer power mult…

In an actual extension of a Henselian discrete valuation, an Eisenstein power-basis generator generates the target valuation ring. Its residue is zero, so every target residue is the image of a constant coefficient from…

The extension relation is ambient data: an algebra, finite-dimensionality, and mathlib's Valuation.HasExtension property. There is deliberately no proof-irrelevant marker object. All invariants and maps are defined once…

This aggregate exposes degree and defectlessness, henselianity, localizations, discrete prolongations, prime-power roots, and uniqueness of extensions.

The integral closure of the base valuation ring supplies the valuation subring used to compare extensions. Local maximal-ideal centers and subsingleton fibers lead to uniqueness criteria, including criteria obtained from…

A local map of valuation rings with the given fraction-field map determines an extension of valuations. Applied to an actual local DVR over the base valuation ring, this supplies the extension property of its normalized…

The local Dedekind fundamental identity only needs discretely valued fields. Completeness and Henselianity play no role once the target valuation ring is a finite module over the base valuation ring.

This file collects theorem-level consequences around finite valued extensions: canonical local-Dedekind degree formulas, uniqueness criteria for extended valuations, and the algebra equivalence identifying an actual inte…

The localized integral closure constructs a discrete extension valuation. Henselianity follows from the simple-root condition on the base valuation ring and uniqueness along algebraic field towers.

The actual localization constructed in LocalizationRing is a DVR in a finite separable extension. Its canonical fraction-field valuation extends the given base valuation, without completeness or Henselian assumptions.

For a local ring R, localizing an R-algebra at a prime above the maximal ideal gives a local map from R. This uses the actual localization and lying-over data, without integrality or finiteness assumptions.

Choose a prime above the base maximal ideal and realize its localization as the image of the injective localization map into the extension field. This subalgebra representation uses the canonical inclusion and scalar tow…

The localized integral closure supplies a discrete extension valuation. Its residue characteristic is the base residue characteristic, so the prime-power root bound applies to every finite extension of a mixed characteri…

Finite separable field extensions carry discrete prolongations of the original valuation. These can use the original value-group universe and preserve the residue characteristic.

Uniqueness is stated up to equivalence of extension valuations. Integral-closure valuation subrings, local centers, and fibers provide concrete criteria, while the corresponding Henselian-field results are transferred to…

This file provides record-free theorems for the integral closure of a complete-DVF valuation ring in a finite separable field extension.

The field norm constructs a discrete extension with the original value group. The complete absolute-value extension supplies adic completeness through its actual norm formula. Separability and residue-field perfection ar…

For a complete rank-one valued field, the field norm gives a valuation on any finite field extension. The strong triangle inequality follows from the actual spectral absolute-value extension. Separability is not needed.

Roots of unity belong to the valuation ring. The cyclotomic valuation bound gives a single exponent annihilating every root of prime-power order, so they form a finite set.

This file contains the lightweight package for a discretely valued field whose valuation ring is Henselian at its maximal ideal.

Every base-field automorphism of a finite extension preserves the actual extension valuation. Henselianity supplies uniqueness of the valuation ring; the finite order of the automorphism then forces equality of values.

This file keeps the Nakayama and finite-module completion consequences away from the lightweight HenselianDVF core.

Hensel lifting supplies primitive roots, while injectivity of torsion reduction transfers finiteness of each primary component in residue characteristic zero.

If the root order is nonzero in the residue field, Hensel lifting and uniqueness make reduction bijective on roots of unity. No completeness or finiteness assumption on the residue field is needed.

The map on all roots of unity is the restriction of the actual residue map on valuation-ring units. It is independent of any chosen exponent. Hensel uniqueness makes this map injective when the residue field has characte…

This file keeps the valuation-extension uniqueness interface separate from the lightweight Henselian-DVF core. The core file is used by Hensel lifting and does not need to import mathlib's full Valuation.HasExtension API…

The value of a nonzero integer is determined by its p-adic order at the residue characteristic. Taking its natural absolute value reduces the formula to the natural-number case, without a characteristic-zero hypothesis.

This module uses the actual mathlib integral closure integralClosure base.toDVF.valuationSubring L. It does not introduce a replacement structure.

The extension is the actual AdjoinRoot (X ^ r - C π) over the fraction field. Eisenstein irreducibility supplies its field structure and power basis; a primitive root of unity supplies the splitting field and Galois prop…

A positive-power binomial X ^ n - C π is Eisenstein at the principal ideal of a prime element. In an integrally closed domain, its image in the fraction field is therefore irreducible. These inputs require no valuation,…

A prime uniformizer supplies an Eisenstein Kummer polynomial. A primitive root of unity makes its actual root extension cyclic Galois. The localized integral closure then supplies the extension valuation, and the Eisenst…

A finite separable extension receives an integer-valued complete discrete valuation. The induced embedding of residue fields preserves characteristic.

The part of a natural number prime to the residue characteristic has nonzero residue and is therefore a unit of the valuation ring. Thus its value is one, and the value of the natural number is determined by its prime-po…

For each natural number greater than one, the image of a discrete valuation contains a nonzero value that is not an nth power. A normalized valuation and uniformizer supply the witness.

Adjoining roots of unity to a finite normal extension preserves normality over the original field. The upper field is the splitting field of the product of a nonzero lower splitting polynomial and X^n - 1.

The maximal ideal of the actual valuation ring supplies an integer-valued discrete valuation on its fraction field. Its valuation subring is the original subring of that same field, without a Henselianity assumption.

The integral closure supplies a complete extension valuation, and its localization supplies an integer-valued discrete extension valuation. Uniqueness identifies their valuation subrings and transports completeness.

Use the existing WithVal field with the rank-one embedding of base 2. The resulting norm has exactly the original valuation ring, transported by WithVal.equiv. The normed structures below are local to this file.

The valuation argument underlying Proposition 2.4 of Bary-Soroker--Nguyen, On the embedding problem for Galois groups (arXiv:1008.1879), specializes here to discrete valuations. At sufficiently large values the leading t…

The residue characteristic has value less than one. Its powers therefore make any field element integral, by the Archimedean property of the multiplicative integers with zero. Completeness is not needed.

Evaluating the prime-power cyclotomic polynomial at one gives the valuation formula. In residue characteristic p, a p-power root reduces to one, giving the positive valuation needed to bound the cyclotomic degree.

For an integer-valued valuation in mixed characteristic, the positive exponent of the residue prime gives the denominator estimates for logarithm and exponential series. Neither completeness nor residue-field finiteness…

This file adds reusable local-ring residue-field lemmas that are used by the Henselian and unramified parts of the DVF library. It keeps mathlib's IsLocalRing.ResidueField.map and IsLocalRing.residue as the primary objec…

The actual torsion-reduction kernel is a p-group. Its elements inject into the finite set of p-power roots of the original field. Finiteness of the residue-field torsion then gives finiteness of all field torsion, withou…

Factor a finite annihilating exponent as p^a times an integer prime to p. A kernel element is an actual principal unit. Its p^a-th power is killed by the prime-to-p factor, hence is one by the geometric-sum argument. Thi…

Mathlib's uniqueness criterion for valuations is expressed through Valuation.IsEquiv: two valuations on the same field are equivalent exactly when they have the same valuation subring. The results here use the ambient va…

The uniformly continuous map on the WithVal models is transported to the actual valuation topologies on the original fields. No completion, finite degree, or choice of normalized absolute value is required.

A valuation-preserving automorphism preserves every basic neighbourhood of zero for the actual topology induced by the valuation. No completeness or discreteness hypothesis is required.

This file records the source facts needed to transport complete-DVF data from a finite subextension to its image inside a common ambient field. The transport is by comapping the valuation along a field equivalence; no va…

A finite family of inequivalent discrete valuations admits simultaneous approximation, with independently prescribed nonzero valuation radii.

The valuation ring is complete in its native subtype topology because that topology is maximal-ideal adic. A compatible norm identifies this ring with the closed unit ball, whose completeness implies completeness of the…

A nonsquare defines a quadratic norm form whose values do not all lie in the two square classes killed by adjoining its square root. The proof normalizes the valuation, minimizes within a unit square class, and then cons…

Hensel's simple-root theorem bounds the precision of a nonsquare near one. For integer-valued valuations, a principal unit of valuation-one difference from one cannot be a square when the value of two is less than one.

An order-preserving permutation of a finite orbit cannot change the valuation value at any point. Thus finite-order automorphisms preserving a valuation class preserve the valuation itself.

A linearly independent family in the residue extension lifts to a linearly independent family upstairs: divide a proposed relation by a coefficient of maximal valuation and reduce. This proves finite residue degree witho…

Mathlib exposes the simple-root form of Hensel's lemma. The statements below turn it into a linear-factor lifting API for a simple residual linear factor.

Chevalley's theorem supplies an extension over every further algebraic field. Uniqueness over the original Henselian base makes this extension unique. The valuation-ring criterion then supplies Henselianity upstairs.

The integral closure is an actual valuation ring. Every extension valuation has this ring of integers, so any two extension valuations are equivalent.

In an algebraic extension, every element or its inverse is integral over a Henselian valuation ring. The argument extends the valuation to an algebraic closure, uses equality of the values of conjugate roots, and bounds…

Public aggregate for the Henselian factorization criterion, polynomial lifting, and uniqueness results for algebraic valuation extensions.

In characteristic p, the maximal ideal is contained in the image of x ↦ x^p - x. Consequently this additive image is open in the valued field.

The localization reduction in the ramification-localization argument passes to the completion of a rank-one nonarchimedean absolute value. the factorization form of Hensel's lemma already supplies the degree-controlled f…

A coprime monic factorization over the residue field gives a point of the universal coprime factorization algebra. This algebra is etale, so its residue point lifts over a Henselian pair. The universal factors give the r…

The Henselian factorization condition and the residual linear-factor lemmas used in the residual linear-factor criterion.

At the kernel of a residue point, an etale algebra has a standard etale localization. The Henselian root lift on that localization restricts to the requested lift on the original algebra.

This file records the coefficientwise Cauchy form of the infinite Hensel approximants. It is the input needed for the adic-completeness step in the coefficientwise proof of Hensel's lemma.

The approximation, correction, and completeness results used to lift coprime factorizations over valuation rings.

This file connects the chosen finite-minimum coefficient to the displayed-factor complete-limit theorem.

This file records the residue-polynomial data used at the start of the proof of Hensel's lemma. The analytic convergence step is kept separate; the lemmas here are the initial lifts and congruences.

The coefficientwise proof of Hensel's lemma chooses, among the finitely many coefficients of f - g₀h₀ and ag₀ + bh₀ - 1, one coefficient of minimum valuation and calls it π. In a valuation ring this is the same algebraic…

This file supplies the explicit endpoint from completeness and nonarchimedeanness, using the principal element selected from the finitely many initial error coefficients in the proof core.

This file supplies the degree estimates for the polynomials fn appearing in the coefficientwise Hensel iteration.

This file supplies the degree estimate for the remainder in the coefficientwise Hensel correction step. It removes the later need to assume separately that the residue of the remainder has small degree.

This file contains the π^n-to-π^(n+1) step in the coefficientwise proof of Hensel's lemma. The preceding files produce the correction congruence modulo the maximal ideal; here it is converted into the actual improvement…

This file isolates the reusable one-step extension in the finite Hensel construction. Compatible prefixes themselves are assembled once, as HenselFactorizationFinitePrefixState, in the next layer.

This file turns the finite Hensel-prefix construction into a recursive family of compatible prefixes. The completion/limit argument is kept for the next layer.

This file records the recursive polynomial iterates used in the proof of Hensel's lemma and the coefficientwise adic estimates needed for the later completion argument.

This file keeps the Hensel limit step in the filtration generated by the chosen chosen element π. This is the route needed for complete valued fields whose maximal ideal is not assumed principal or adically separated.

This file packages the algebraic correction, degree truncation, and π-power update into the single step used recursively in the proof of Hensel's lemma.

This file contains the finite coefficient-cutting step used in the proof of Hensel's lemma: after the division step, coefficients already zero in the residue field may be omitted to impose the required degree bound.

This file carries the displayed C π factors from the infinite Hensel prefixes through the maximal-ideal complete-limit argument.

Over a Henselian valued field of residue characteristic zero, a fixed finite residue extension determines one finite intermediate field in which its primitive roots of unity lift for every positive order. The field is co…

This file isolates the residue-polynomial input used in the irreducible-polynomial coefficient estimate. For the closed-unit-ball valuation ring attached to a nonarchimedean absolute value, coefficients of value < 1 redu…

This file applies the explicit Hensel lemma from the coefficientwise Hensel construction to the normalized residue input constructed by the coefficient-bound lemmas. The result here is the core contradiction for irreduci…

This file isolates the algebraic condition used in the factor-lifting criterion. The condition is the exact condition: a monic polynomial whose reduction is a product of relatively prime monic polynomials has monic facto…

This file extracts the Newton--Vieta part of the converse Hensel argument from the unique-extension criterion. No uniqueness of valuation extensions is used here: once all conjugate roots have the same value, a primitive…

A simple residual root gives a coprime linear factor. Primitive factor lifting produces an actual factor of degree one. Its leading coefficient reduces to one, so it is a unit and its linear root belongs to the valuation…

The norm of a finite extension is preserved by every base-field automorphism when the nonarchimedean base valuation ring is Henselian. Completeness of the base field is not required.

This file isolates the common algebraic last step in the unique-extension and factor-lifting criteria. The proof first proves that the reduction of every primitive irreducible factor is either constant or has full degree…

The construction calls a polynomial over a valuation ring primitive when its reduction modulo the maximal ideal is nonzero. The lemma below identifies that condition with the divisibility notion used by mathlib's Gauss l…

In a Henselian valued field, every element closer to one than the square of the value of a nonzero integer n is an nth power. Rescaling the binomial polynomial gives a simple residual root, even when n is not a residue u…

Coefficient pullback and the induced quotient equivalence transport simple roots. The Jacobson-radical condition transports along the same ring map.

Reduction on roots of unity of order invertible in the residue field is injective and, for a Henselian valuation ring, surjective. Roots of nonzero order in the field also belong to the valuation ring.

The Henselian ring assumption now supplies the actual coprime factors. The valuation factorization criterion then extends the monic result to all primitive polynomials, with the prescribed reductions and degree bounds.

The simple-root condition for a Henselian pair lifts a residue point of a standard étale algebra to the base ring. The defining monic polynomial and its derivative condition supply the Hensel input, and the Jacobson cond…

Valuations are regarded valuations up to equivalence. Accordingly, uniqueness on an algebraic extension is stated as literal uniqueness of its valuation subring. This is the same endpoint used in the finite norm-formula…

This file supplies the last Galois/Newton-polygon input in the converse of the unique-extension criterion. Uniqueness of the extension valuation ring makes it invariant under the finite Galois group of a splitting field.…

This file develops the Galois/residue input in the converse direction. A monic polynomial over the base valuation ring whose roots lie in a splitting field in fact splits over every extension valuation ring: its roots ar…

Artin's monic coprime-factor lifting criterion implies the exact primitive factorization form of Hensel's lemma from the primitive factorization definition.

Equivalences of local rings preserve the maximal ideal and all of its powers. The resulting membership criterion is useful when transporting principal-unit filtrations between equivalent valuation rings.

A finite normal extension is the splitting field of a nonzero polynomial. If the polynomial supplied by the standard existence theorem is zero, the constant polynomial one has the same empty root set and generates the sa…

If 1 < v (x ^ n - x) and n > 1, the leading term determines its value, which must be an n-th power. This gives an obstruction using the logarithmic exponent of an integer-valued valuation.

In residue characteristic p, if a p-power of a field element is a principal unit, so is the element. This uses neither discreteness nor completeness of the valuation, and does not require the residue field to be perfect.

For a principal unit x, reduction of the geometric sum of its first n powers is n. If n is nonzero in the residue field, this sum is nonzero. The geometric-sum identity then makes x^n = 1 imply x = 1. No Henselianity, di…

A valuation subring of an algebraically closed field has algebraically closed residue field. Lift a monic residue polynomial, choose its root in the ambient field, and use integral closedness to realize that same root in…

This file contains the algebraic and topological projective-limit descriptions of unit groups of adically complete rings and complete discrete valuation rings. The underlying adic ring inverse-limit theory lives in AdicC…

This file contains the algebraic and topological projective-limit descriptions of adically complete rings, complete discrete valuation rings, and their unit groups.

An additive endomorphism which sends I ^ n into I ^ (n + 1) is topologically nilpotent for the I-adic topology. Completeness therefore solves the affine fixed-point equation x = b + T x uniquely. The proof uses the succe…

Aggregate for the ValuationTheory.Topology folder.

The elementary inverse limits used in the local-field structure development are subobjects of dependent products: their elements are precisely the families preserved by every transition map. Keeping this construction at…

This file adds only the two topology lemmas used by valuation theory. The underlying type, topology, and basic API come directly from Mathlib. Algebraic structures needed on a particular topology-indexed copy are install…

The pullback of an extension valuation ring by a ground-field automorphism is again an extension valuation ring. Hence uniqueness forces the chosen ring to be fixed by every automorphism of the extension field. This is t…

This file supplies the common source used in the valuation-topology and adic-completeness arguments: on a rank-one discrete valued field, the native topology of the valuation ring is its maximal-ideal adic topology. Cons…