MultiplicativelyIndependent.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 10 curated AI-written annotations and 7190 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, Formal Conjectures paper, arXiv v1

5 declarations, 0 contain sorry, 0 declared as axioms

Multiplicatively independent integers

Two integers $p, q \ge 2$ are multiplicatively independent if $\log p / \log q$ is irrational, equivalently if $p^m = q^n$ holds only for $m = n = 0$. The condition separates bases whose expansions carry unrelated information, as in Cobham's theorem and in Furstenberg's $\times p$, $\times q$ problems.

For a family of more than two integers the notion is the joint one: no nonzero integer tuple n satisfies ∏ i, b i ^ n i = 1. That is strictly stronger than pairwise independence, and is what results such as Adamczewski–Faverjon's Mahler-method theorems assume.

Main definitions

Nat.MultiplicativelyIndependent: the relation for a pair of integers.
Nat.MultiplicativelyIndependentFamily: the joint relation for a family of integers.

Imports (3)

Imported by 1 file

FormalConjecturesForMathlib.lean

def Nat.MultiplicativelyIndependent Two integers $p, q \ge 2$ are multiplicatively independent if $\log p / \log q$ is irrational, equivalently if $p^m = q^n$ holds only for $m = n = 0$ line 48 source
Source documentation
Two integers $p, q \ge 2$ are multiplicatively independent if $\log p / \log q$ is irrational, equivalently if $p^m = q^n$ holds only for $m = n = 0$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Irrational, HDiv.hDiv, Real, Real.log
5 instances, coercions and auxiliary constants left out.
```
def MultiplicativelyIndependent (p q : ℕ) : Prop := Irrational (Real.log p / Real.log q)
```
theorem Nat.MultiplicativelyIndependent.symm Multiplicative independence is symmetric line 51 source
Source documentation
Multiplicative independence is symmetric.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.MultiplicativelyIndependent
Proof uses: Eq.mpr, Irrational, HDiv.hDiv, Real, Real.log, id, Eq, congrArg, Nat.MultiplicativelyIndependent.eq_1, Inv.inv, Eq.symm, inv_div, Irrational.inv
12 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem MultiplicativelyIndependent.symm {p q : ℕ} (h : MultiplicativelyIndependent p q) :
    MultiplicativelyIndependent q p := by
…
```
Mentions: Nat.MultiplicativelyIndependent
def Nat.MultiplicativelyIndependentFamily A family of integers is multiplicatively independent if there is no nonzero tuple of integers line 65 source
Source documentation
A family of integers is multiplicatively independent if there is no nonzero tuple of integers $(n_i)$ with $\prod_i b_i^{n_i} = 1$; equivalently, the numbers $\log b_i$ are linearly independent over $\mathbb{Q}$, which is the form used here.
This is the joint notion, which is strictly stronger than pairwise multiplicative independence of the b i (Nat.MultiplicativelyIndependentFamily.pairwise). For a family of two it agrees with Nat.MultiplicativelyIndependent, by Nat.MultiplicativelyIndependent.family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: LinearIndependent, Rat, Real, Real.log
19 instances, coercions and auxiliary constants left out.
```
def MultiplicativelyIndependentFamily {ι : Type*} (b : ι → ℕ) : Prop :=
…
```
theorem Nat.MultiplicativelyIndependentFamily.pairwise A multiplicatively independent family is pairwise multiplicatively independent line 69 source
Source documentation
A multiplicatively independent family is pairwise multiplicatively independent.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.MultiplicativelyIndependentFamily, Pairwise, Nat.MultiplicativelyIndependent
Proof uses: Ne, Membership.mem, Real, Set, Set.range, Rat, HDiv.hDiv, Real.log, False, Eq, OfNat.ofNat, LinearIndependent.ne_zero, Iff.mp, LinearIndepOn, Insert.insert, Singleton.singleton, HSMul.hSMul, linearIndepOn_pair_iff, Ne.symm, LinearIndependent.linearIndepOn and 7 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem MultiplicativelyIndependentFamily.pairwise {ι : Type*} {b : ι → ℕ}
    (h : MultiplicativelyIndependentFamily b) :
    Pairwise fun i j => MultiplicativelyIndependent (b i) (b j) := by
…
```
Mentions: Nat.MultiplicativelyIndependentFamily, Nat.MultiplicativelyIndependent
theorem Nat.MultiplicativelyIndependent.family A multiplicatively independent pair is a multiplicatively independent family line 78 source
Source documentation
A multiplicatively independent pair is a multiplicatively independent family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Nat.MultiplicativelyIndependent, Nat.MultiplicativelyIndependentFamily, Fin, Nat.succ, OfNat.ofNat, Matrix.vecCons, Matrix.vecEmpty
Proof uses: Ne, Real, Real.log, Eq, Eq.mp, Irrational, HDiv.hDiv, congrArg, div_zero, Nat.MultiplicativelyIndependent.eq_1, Exists.intro, Rat, Mathlib.Meta.NormNum.isNat_eq_true, Mathlib.Meta.NormNum.isNat_ratCast, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Nat.cast_zero, Eq.mpr, LinearIndependent, id and 19 more
98 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
```
theorem MultiplicativelyIndependent.family {p q : ℕ} (h : MultiplicativelyIndependent p q) :
    MultiplicativelyIndependentFamily ![p, q] := by
…
```
Mentions: Nat.MultiplicativelyIndependent, Nat.MultiplicativelyIndependentFamily