LocalUnits.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

11 declarations, 0 contain sorry, 0 declared as axioms

Uniformisers in adic completions

Choices of uniformisers in the adic completion K_v of a Dedekind domain at a finite place v, together with the basic API.

Main definitions

HeightOneSpectrum.adicCompletionUniformizer: a chosen uniformiser of the adic completion at v.

Imports (2)

Imported by 2 files

def IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer A uniformiser associated to v in the completion Kᵥ line 40 source
Source documentation
A uniformiser associated to v in the completion Kᵥ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: RingHom, Algebra.algebraMap, Exists.choose, Eq, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, WithZero.exp, Neg.neg, OfNat.ofNat, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer
25 instances, coercions and auxiliary constants left out.
```
noncomputable def adicCompletionUniformizer (v : HeightOneSpectrum A) :
    v.adicCompletion K :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.v_adicCompletionUniformizer line 45 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Eq, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Valued.v, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer, Equiv, Multiplicative.ofAdd, Neg.neg, OfNat.ofNat
Proof uses: Exists.choose, IsDedekindDomain.HeightOneSpectrum.valuation, WithZero.exp, IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer, Exists.choose_spec, Eq.mp, IsDedekindDomain.HeightOneSpectrum.adicCompletion.ofCompletion, WithVal, WithVal.toVal, congrArg, Eq.symm, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'
53 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegersUniformizer A uniformiser associated to v in the integers of the completion Kᵥ line 54 source
Source documentation
A uniformiser associated to v in the integers of the completion Kᵥ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers
Proof uses: Subtype.mk, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
noncomputable def adicCompletionIntegersUniformizer (v : HeightOneSpectrum A) :
    v.adicCompletionIntegers K :=
…
```
lemma IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer_ne_zero line 59 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Ne, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer, OfNat.ofNat
Proof uses: Eq, False.elim, False, Eq.mp, WithZero, Multiplicative, Int, Equiv, Multiplicative.ofAdd, Neg.neg, Valuation, Valued.v, Eq.trans, Inv.inv, congrArg, map_zero, IsDedekindDomain.HeightOneSpectrum.v_adicCompletionUniformizer, eq_of_heq, outParam, DFunLike and 4 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
def IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizerUnit A uniformiser associated to v in the units of the completion Kᵥ line 67 source
Source documentation
A uniformiser associated to v in the units of the completion Kᵥ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: Units.mk0, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer_ne_zero
13 instances, coercions and auxiliary constants left out.
```
noncomputable def adicCompletionUniformizerUnit (v : HeightOneSpectrum A) :
    (v.adicCompletion K)ˣ :=
…
```
def IsDedekindDomain.FiniteAdeleRing.localUniformiser localUniformiser v is an adele which is 1 at all finite places except v, where it is a uniformiser line 77 source
Source documentation
localUniformiser v is an adele which is 1 at all finite places except v, where it is a uniformiser.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, DecidableEq, IsDedekindDomain.FiniteAdeleRing
Proof uses: Subtype.mk, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.Eventually, Membership.mem, Set, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Pi.mulSingle, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer
18 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable def localUniformiser (v : HeightOneSpectrum A) [DecidableEq (HeightOneSpectrum A)] :
    FiniteAdeleRing A K :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.localUniformiser_eval line 85 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, DecidableEq, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.localUniformiser, Pi.mulSingle, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.localUniformiserUnit localUniformiser v is an idele which is 1 at all finite places except v, where it is a uniformiser line 92 source
Source documentation
localUniformiser v is an idele which is 1 at all finite places except v, where it is a uniformiser.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, DecidableEq, Units, IsDedekindDomain.FiniteAdeleRing
Proof uses: Units.mk, IsDedekindDomain.FiniteAdeleRing.localUniformiser, Subtype.mk, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.Eventually, Membership.mem, Set, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Pi.mulSingle, Inv.inv, IsDedekindDomain.HeightOneSpectrum.adicCompletionUniformizer
30 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
```
noncomputable def localUniformiserUnit (v : HeightOneSpectrum A)
    [DecidableEq (HeightOneSpectrum A)] :
    (FiniteAdeleRing A K)ˣ :=
…
```
def IsDedekindDomain.FiniteAdeleRing.localUnit localUnit K α for α : (v.adicCompletion K)ˣ, is the finite idele which is α at v and 1 elsewhere line 115 source
Source documentation
localUnit K α for α : (v.adicCompletion K)ˣ, is the finite idele which is α at v and 1 elsewhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, DecidableEq, IsDedekindDomain.FiniteAdeleRing
Proof uses: Units.mk, Subtype.mk, Filter.Eventually, Membership.mem, Set, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Pi.mulSingle, Inv.inv
33 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
noncomputable def localUnit {v : HeightOneSpectrum A} (α : (v.adicCompletion K)ˣ)
    [DecidableEq (HeightOneSpectrum A)] :
    (FiniteAdeleRing A K)ˣ :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.localUnit_eval_of_eq line 139 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, DecidableEq, Eq, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.localUnit
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Pi.mulSingle_eq_same, eq_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma IsDedekindDomain.FiniteAdeleRing.localUnit_eval_of_ne line 144 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsDedekindDomain, Field, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Units, IsDedekindDomain.HeightOneSpectrum.adicCompletion, DecidableEq, Ne, Eq, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.localUnit, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Pi.mulSingle_eq_of_ne, Not, False, eq_false, not_false_eq_true, eq_self
32 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.