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

`ℚ` inside the restricted product of the `ℚ_p`

We embed ℚ diagonally in the restricted product Πʳ_p [ℚ_[p], ℤ_[p]], and identify rationals with their image (the elements with bounded p-denominator).

Imports (11)

Imported by 2 files

theorem Padic.setOf_norm_one_lt_finite line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Rat, Set.Finite, Nat.Primes, Set.ofPred, LT.lt, Real, OfNat.ofNat, Norm.norm, Padic, Nat, Nat.Prime, Padic.instFactPrimeValNat
Proof uses: Set.Finite.subset, Not, Dvd.dvd, Rat.den, False, Set.Finite.of_finite_image, Subtype, Finset, Nat.primeFactors, of_eq_true, Set.image, Membership.mem, Set, Eq, Eq.mpr, And, id, Eq.trans, Ne, congrArg and 18 more
39 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.padic_valuation_neg_of_mem_indexSupport line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Membership.mem, Finset, RestrictedProduct.indexSupport, Subtype, LT.lt, Int, Padic.valuation, OfNat.ofNat
Proof uses: Mathlib.Tactic.Contrapose.contrapose₁, Eq.mpr, Not, LE.le, id, Eq, implies_congr, Eq.refl, Eq.trans, congrArg, Real, Norm.norm
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.padicNatDen The smallest positive natural n : ℕ for which x p * n is a p-adic integer for all p line 59 source
Source documentation
The smallest positive natural n : ℕ for which x p * n is a p-adic integer for all p.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite
Proof uses: Finset.prod, RestrictedProduct.indexSupport, Subtype, HPow.hPow, Int.natAbs, Padic.valuation
19 instances, coercions and auxiliary constants left out.
```
noncomputable def padicNatDen
    (x : Πʳ (p : Nat.Primes), [ℚ_[p], subring p]) : ℕ :=
…
```
theorem RestrictedProduct.padicNatDen_ne_zero line 63 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Ne, RestrictedProduct.padicNatDen, OfNat.ofNat
Proof uses: Eq.mpr, Finset.prod, RestrictedProduct.indexSupport, Subtype, HPow.hPow, Int.natAbs, Padic.valuation, id, Eq, congrArg, RestrictedProduct.padicNatDen.eq_1, Membership.mem, Finset, propext, Finset.prod_ne_zero_iff, of_eq_true, Not, Eq.trans, False, True and 8 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.padicNatDen_norm_of_mem line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Membership.mem, Finset, RestrictedProduct.indexSupport, Eq, Real, Norm.norm, RestrictedProduct.padicNatDen, HPow.hPow, Int, Neg.neg, Int.natAbs and 1 more
Proof uses: Eq.mpr, Finset.prod, Subtype, id, congrFun', congrArg, Eq.trans, Nat.cast_prod, Finset.prod_congr, Eq.refl, Nat.cast_pow, norm_prod, norm_pow, Finset.prod_eq_single_of_mem, Ne, OfNat.ofNat, Iff.mpr, Nat.Coprime, Padic.norm_natCast_eq_one_iff, Nat.coprime_primes and 21 more
122 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.padicNatDen_norm_of_notMem line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Not, Membership.mem, Finset, RestrictedProduct.indexSupport, Eq, Real, Norm.norm, RestrictedProduct.padicNatDen, OfNat.ofNat
Proof uses: Eq.mpr, Finset.prod, Subtype, HPow.hPow, Int.natAbs, Padic.valuation, id, congrFun', congrArg, Eq.trans, Nat.cast_prod, Finset.prod_congr, Eq.refl, Nat.cast_pow, norm_prod, norm_pow, Finset.prod_eq_one, Iff.mpr, Nat.Coprime, Padic.norm_natCast_eq_one_iff and 9 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.padicNatDen_norm_mul_le_one line 92 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, LE.le, Real, Norm.norm, HMul.hMul, Rat, RestrictedProduct.padicNatDen, OfNat.ofNat
Proof uses: dite, Membership.mem, Finset, RestrictedProduct.indexSupport, Subtype, Eq, Classical.propDecidable, of_eq_true, Eq.trans, True, congrFun', congrArg, congr, Rat.cast_natCast, MulZeroClass.mul_zero, norm_zero, Not, Eq.mpr, HPow.hPow, Int and 30 more
151 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.padicNum The element of (p : Nat.Primes) → ℤ_[p] obtained by multiplying by padicNatDen line 104 source
Source documentation
The element of (p : Nat.Primes) → ℤ_[p] obtained by multiplying by padicNatDen.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, PadicInt
Proof uses: Subtype.mk, Membership.mem, HMul.hMul, RestrictedProduct.padicNatDen, RestrictedProduct.padicNatDen_norm_mul_le_one
22 instances, coercions and auxiliary constants left out.
```
noncomputable def padicNum (x : Πʳ (p : Nat.Primes), [ℚ_[p], subring p]) (p : Nat.Primes) : ℤ_[p] :=
…
```
theorem RestrictedProduct.padic_exists_sub_mem_padicInt line 108 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Exists, Rat, Membership.mem, HSub.hSub
Proof uses: Subtype, Finset, RestrictedProduct.indexSupport, ZMod, HPow.hPow, Int.natAbs, Padic.valuation, RingHom, PadicInt, PadicInt.toZModPow, RestrictedProduct.padicNum, Pairwise, Nat.Coprime, Ne, Nat.coprime_pow_primes, Subtype.property, Eq.mpr, Not, Eq, id and 124 more
206 instances, coercions and auxiliary constants left out.

Tactic trace: 28 steps
Open to load the checked before-and-after goal states.
instance RestrictedProduct.(instance at line 145) line 145 source
theorem RestrictedProduct.padic_exists_sub_mem_structureSubring line 155 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: RestrictedProduct, Nat.Primes, Padic, Nat, Nat.Prime, RestrictedProduct.instFactPrimeValNat, Subring, PadicInt.subring, Filter.cofinite, Exists, Rat, Membership.mem, Subtype, RestrictedProduct.structureSubring, HSub.hSub, RingHom, Algebra.algebraMap
Proof uses: RestrictedProduct.padic_exists_sub_mem_padicInt, Exists.intro, Iff.mpr, RestrictedProduct.mem_structureSubring_iff, Eq.mpr, LE.le, Real, Norm.norm, OfNat.ofNat, id, Eq, Eq.mp, Neg.neg, Eq.trans, congrArg, neg_sub, Subring.neg_mem
72 instances, coercions and auxiliary constants left out.

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

FLT/NumberField/Padics/RestrictedProduct.lean

ℚ inside the restricted product of the ℚ_p

`FLT/NumberField/Padics/RestrictedProduct.lean`

`ℚ` inside the restricted product of the `ℚ_p`