Basic.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

8 declarations, 0 contain sorry, 0 declared as axioms

Valuative relations

Material destined for Mathlib.

Imports (4)

Imported by 3 files

theorem ValuativeRel.valuation_natCast_le_one Naturals have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation line 27 source
Source documentation
Naturals have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, ValuativeRel, Nat, LE.le, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat
Proof uses: Iff.mp, Membership.mem, Subring, Valuation.integer, Valuation.mem_integer_iff, natCast_mem
44 instances, coercions and auxiliary constants left out.
```
theorem valuation_natCast_le_one (m : ℕ) : valuation R (m : R) ≤ 1 :=
…
```
theorem ValuativeRel.valuation_intCast_le_one Integers have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation line 32 source
Source documentation
Integers have valuation at most 1: they lie in the integer subring (valuation R).integer of the valuation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, ValuativeRel, Int, LE.le, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat
Proof uses: Iff.mp, Membership.mem, Subring, Valuation.integer, Valuation.mem_integer_iff, intCast_mem
37 instances, coercions and auxiliary constants left out.
```
theorem valuation_intCast_le_one (m : ℤ) : valuation R (m : R) ≤ 1 :=
…
```
theorem ValuativeRel.exists_pow_valuation_lt Powers of an element of the open unit disc become arbitrarily small line 40 source
Source documentation
Powers of an element of the open unit disc become arbitrarily small. This is where the rank-one hypothesis on the value group enters (via the strictly monotone embedding into ℝ≥0 provided by IsRankLeOne, where the statement is the usual archimedean one): an abstract value group of higher rank need not be archimedean, and the statement would be false.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, ValuativeRel, ValuativeRel.IsRankLeOne, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, Units, Exists, Nat, HPow.hPow
Proof uses: Eq, Ne, Or, eq_or_ne, Exists.intro, of_eq_true, Eq.trans, True, congrFun', congrArg, pow_one, ValuativeRel.RankLeOneStruct, Nonempty, ValuativeRel.IsRankLeOne.nonempty, NNReal, MonoidWithZeroHom, ValuativeRel.RankLeOneStruct.emb, exists_pow_lt_of_lt_one, Eq.mp, map_zero and 10 more
81 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem exists_pow_valuation_lt [IsRankLeOne R] (q : R) (hq : valuation R q < 1)
    (γ : (ValueGroupWithZero R)ˣ) : ∃ N : ℕ, valuation R q ^ N < γ := by
…
```
theorem ValuativeRel.adicValuation_lt_one_iff Documented declaration: adicValuation_lt_one_iff line 68 source
Source documentation
On an integral element, the adic valuation attached to the maximal ideal of 𝒪[K] is less than 1 exactly when the canonical valuation is: both detect membership in the maximal ideal, i.e. non-unitality in 𝒪[K].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, IsDiscreteValuationRing, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, IsFractionRing, Iff, LT.lt, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, RingHom, Algebra.algebraMap and 1 more
Proof uses: Eq.mpr, Ideal, IsDedekindDomain.HeightOneSpectrum.asIdeal, id, Eq, congrArg, propext, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem, Iff.intro, Iff.mp, Not, IsUnit, Valuation.Integer.not_isUnit_iff_valuation_lt_one, Set, nonunits, mem_nonunits_iff, IsLocalRing.maximalIdeal, IsLocalRing.mem_maximalIdeal, Iff.mpr
127 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem adicValuation_lt_one_iff {x : (valuation K).integer} :
    (IsDiscreteValuationRing.maximalIdeal (valuation K).integer).valuation K
        (algebraMap (valuation K).integer K x) < 1 ↔
      valuation K (algebraMap (valuation K).integer K x) < 1 := by
…
```
theorem ValuativeRel.adicValuation_eq_one_iff On an integral element, the adic valuation attached to the maximal ideal of 𝒪[K] equals 1 exactly when the canonical valuation does: both detect unitality in 𝒪[K] line 80 source
Source documentation
On an integral element, the adic valuation attached to the maximal ideal of 𝒪[K] equals 1 exactly when the canonical valuation does: both detect unitality in 𝒪[K].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, ValuativeRel, IsDiscreteValuationRing, Subtype, Membership.mem, Subring, Valuation.integer, ValuativeRel.ValueGroupWithZero, ValuativeRel.valuation, IsFractionRing, Iff, Eq, WithZero, Multiplicative, Int, Valuation, IsDedekindDomain.HeightOneSpectrum.valuation, IsDiscreteValuationRing.maximalIdeal, RingHom, Algebra.algebraMap and 1 more
Proof uses: Eq.mpr, Not, Ideal, IsDedekindDomain.HeightOneSpectrum.asIdeal, id, congrArg, propext, IsDedekindDomain.HeightOneSpectrum.valuation_eq_one_iff_notMem, Iff.intro, Iff.mp, IsUnit, Valuation.Integers.isUnit_iff_valuation_eq_one, Valuation.integer.integers, Classical.byContradiction, Iff.mpr, IsLocalRing.maximalIdeal, Set, nonunits, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff
112 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem adicValuation_eq_one_iff {x : (valuation K).integer} :
    (IsDiscreteValuationRing.maximalIdeal (valuation K).integer).valuation K
        (algebraMap (valuation K).integer K x) = 1 ↔
      valuation K (algebraMap (valuation K).integer K x) = 1 := by
…
```
theorem ValuativeExtension.valuation_algebraMap_le_one A valuative extension maps the closed unit disc into the closed unit disc; in other words, algebraMap A B maps the ring of integers 𝒪[A] into 𝒪[B] line 114 source
Source documentation
A valuative extension maps the closed unit disc into the closed unit disc; in other words, algebraMap A B maps the ring of integers 𝒪[A] into 𝒪[B].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ring, ValuativeRel, Algebra, ValuativeExtension, LE.le, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: Eq.mp, MonoidWithZeroHom, ValuativeExtension.mapValueGroupWithZero, congr, congrArg, ValuativeExtension.mapValueGroupWithZero_valuation, map_one, StrictMono.monotone, ValuativeExtension.mapValueGroupWithZero_strictMono
43 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_algebraMap_le_one {x : A} (hx : valuation A x ≤ 1) :
    valuation B (algebraMap A B x) ≤ 1 := by
…
```
theorem ValuativeExtension.valuation_algebraMap_lt_one A valuative extension maps the open unit disc into the open unit disc; in other words, algebraMap A B maps the maximal ideal of 𝒪[A] into that of 𝒪[B] line 120 source
Source documentation
A valuative extension maps the open unit disc into the open unit disc; in other words, algebraMap A B maps the maximal ideal of 𝒪[A] into that of 𝒪[B].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ring, ValuativeRel, Algebra, ValuativeExtension, LT.lt, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: Eq.mp, MonoidWithZeroHom, ValuativeExtension.mapValueGroupWithZero, congr, congrArg, ValuativeExtension.mapValueGroupWithZero_valuation, map_one, ValuativeExtension.mapValueGroupWithZero_strictMono
48 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_algebraMap_lt_one {x : A} (hx : valuation A x < 1) :
    valuation B (algebraMap A B x) < 1 := by
…
```
theorem ValuativeExtension.valuation_algebraMap_eq_one A valuative extension maps the unit circle into the unit circle; in other words, algebraMap A B maps units of 𝒪[A] to units of 𝒪[B] line 126 source
Source documentation
A valuative extension maps the unit circle into the unit circle; in other words, algebraMap A B maps units of 𝒪[A] to units of 𝒪[B].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Ring, ValuativeRel, Algebra, ValuativeExtension, Eq, ValuativeRel.ValueGroupWithZero, Valuation, ValuativeRel.valuation, OfNat.ofNat, RingHom, Algebra.algebraMap
Proof uses: Eq.mpr, MonoidWithZeroHom, ValuativeExtension.mapValueGroupWithZero, id, congrArg, Eq.symm, ValuativeExtension.mapValueGroupWithZero_valuation, map_one, Eq.refl
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem valuation_algebraMap_eq_one {x : A} (hx : valuation A x = 1) :
    valuation B (algebraMap A B x) = 1 := by
…
```