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

26 declarations, 0 contain sorry, 0 declared as axioms

Bases

References:

[Er56](Erdős, P., Problems and results in additive number theory. Colloque sur la Théorie des Nombres, Bruxelles, 1955 (1956), 127-137.)

Imports (5)

Imported by 1 file

FormalConjecturesForMathlib.lean

def Set.IsMulBasisOfOrder line 45 source
no axioms what this means
Statement uses: CommMonoid, Set, Nat
Proof uses: Membership.mem, HPow.hPow
8 instances, coercions and auxiliary constants left out.
def Set.IsMulBasis An additive basis of some order line 49 source
Source documentation
An additive basis of some order.

no axioms what this means
Statement uses: CommMonoid, Set
Proof uses: Exists, Nat, Set.IsMulBasisOfOrder
```
def IsMulBasis (A : Set M) : Prop := ∃ n, A.IsMulBasisOfOrder n
…
```
lemma Set.IsMulBasisOfOrder.isMulBasis line 52 source
no axioms what this means
Statement uses: CommMonoid, Set, Nat, Set.IsMulBasisOfOrder, Set.IsMulBasis
Proof uses: Exists.intro
lemma Set.isMulBasisOfOrder_iff line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Iff, Set.IsMulBasisOfOrder, Exists, Fin, Membership.mem, Eq, Finset.prod, Finset.univ
Proof uses: Finset, Set.mem_finsetProd, of_eq_true, Eq.trans, And, True, congr, congrArg, forall_congr, HPow.hPow, propext, id, Eq.mp, congrFun', Finset.card, Finset.prod_const, Fintype.card_fin, funext, exists_prop_congr, Iff.of_eq and 3 more
16 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.not_isMulBasisOfOrder_zero No set is an additive basis of order 0 line 62 source
Source documentation
No set is an additive basis of order 0.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nontrivial, Not, Set.IsMulBasisOfOrder, OfNat.ofNat, Nat
Proof uses: of_eq_true, Eq.trans, Exists, Eq, True, congrArg, Fin, Membership.mem, Finset.prod, Finset.univ, forall_congr, funext, propext, exists_prop_congr, Iff.of_eq, congrFun', Finset.prod_congr, EmptyCollection.emptyCollection, Finset, Finset.univ_eq_empty and 1 more
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma not_isMulBasisOfOrder_zero [Nontrivial M] : ¬A.IsMulBasisOfOrder 0 := by
…
```
lemma Set.isMulBasisOfOrder_one_iff line 66 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Iff, Set.IsMulBasisOfOrder, OfNat.ofNat, Nat, Eq, Set.univ
Proof uses: of_eq_true, Eq.trans, Membership.mem, True, congr, congrArg, forall_congr, HPow.hPow, congrFun', pow_one, iff_self
12 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.isMulBasisOfOrder_two_iff line 72 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Iff, Set.IsMulBasisOfOrder, OfNat.ofNat, Nat, Membership.mem, HMul.hMul
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, forall_congr, HPow.hPow, pow_two, iff_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Set.IsAsymptoticMulBasisOfOrder line 80 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat
Proof uses: Filter.Eventually, Membership.mem, HPow.hPow, Filter.cofinite
8 instances, coercions and auxiliary constants left out.
def Set.IsAsymptoticMulBasis An asymptotic additive basis of some order line 84 source
Source documentation
An asymptotic additive basis of some order.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set
Proof uses: Exists, Nat, Set.IsAsymptoticMulBasisOfOrder
```
def IsAsymptoticMulBasis (A : Set M) : Prop := ∃ n, A.IsAsymptoticMulBasisOfOrder n
…
```
lemma Set.IsAsymptoticMulBasisOfOrder.isAsymptoticMulBasis line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Set.IsAsymptoticMulBasisOfOrder, Set.IsAsymptoticMulBasis
Proof uses: Exists.intro
lemma Set.IsMulBasisOfOrder.isAsymptoticMulBasisOfOrder line 91 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Set.IsMulBasisOfOrder, Set.IsAsymptoticMulBasisOfOrder
Proof uses: Filter.Eventually.of_forall, Membership.mem, HPow.hPow, Filter.cofinite
8 instances, coercions and auxiliary constants left out.
lemma Set.IsMulBasis.isAsymptoticMulBasis line 95 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Set.IsMulBasis, Set.IsAsymptoticMulBasis
Proof uses: Nat, Set.IsMulBasisOfOrder, Exists.intro, Set.IsAsymptoticMulBasisOfOrder, Set.IsMulBasisOfOrder.isAsymptoticMulBasisOfOrder
1 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_iff_prod line 103 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Iff, Set.IsAsymptoticMulBasisOfOrder, Filter.Eventually, Exists, Fin, Membership.mem, Eq, Finset.prod, Finset.univ, Filter.cofinite
Proof uses: Finset, Set.mem_finsetProd, of_eq_true, Eq.trans, Set.Finite, Set.ofPred, Not, True, congr, congrArg, HPow.hPow, And, congrFun', Filter, funext, propext, id, Eq.mp, forall_congr, Finset.card and 7 more
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_two_iff line 114 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Iff, Set.IsAsymptoticMulBasisOfOrder, OfNat.ofNat, Nat, Filter.Eventually, Membership.mem, HMul.hMul, Filter.cofinite
Proof uses: of_eq_true, Eq.trans, Set.Finite, Set.ofPred, Not, True, congr, congrArg, HPow.hPow, congrFun', Filter, funext, pow_two, iff_self
21 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.IsAsymptoticMulBasisOfOrder.of_finite line 119 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Finite, Set.IsAsymptoticMulBasisOfOrder
Proof uses: of_eq_true, Filter.Eventually, Membership.mem, HPow.hPow, Filter.cofinite, Eq.trans, Bot.bot, Filter, True, congrArg, Filter.cofinite_eq_bot
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.not_isAsymptoticMulBasisOfOrder_zero line 125 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Infinite, Not, Set.IsAsymptoticMulBasisOfOrder, OfNat.ofNat, Nat
Proof uses: Eq.mpr, Set.Infinite, Set.ofPred, Eq, id, Eq.trans, congrArg, Filter.Eventually, Membership.mem, HPow.hPow, Filter.cofinite, Set.Finite, congrFun', Filter, funext, pow_zero, Set.infinite_of_finite_compl, of_eq_true, Compl.compl, Singleton.singleton and 2 more
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.IsAsymptoticMulBasisOfOrder.ne_zero line 129 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Infinite, Set.IsAsymptoticMulBasisOfOrder, Ne, OfNat.ofNat
Proof uses: Eq, False, False.elim, Eq.mp, Eq.symm
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.IsAsymptoticMulBasisOfOrder.nonempty line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, Infinite, Set.IsAsymptoticMulBasisOfOrder, Set.Nonempty
Proof uses: Classical.byContradiction, Not, False.elim, False, Eq.mp, Eq.trans, Filter.Eventually, Membership.mem, HPow.hPow, Filter.cofinite, Set.Finite, Set.ofPred, congrFun', Filter, congrArg, funext, EmptyCollection.emptyCollection, Eq, Set.empty_pow, of_eq_true and 7 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_one_iff line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Iff, Set.IsAsymptoticMulBasisOfOrder, OfNat.ofNat, Nat, Set.Finite, Compl.compl
Proof uses: of_eq_true, Set.ofPred, Not, Membership.mem, Eq.trans, True, congrFun', congrArg, Filter.Eventually, HPow.hPow, Filter.cofinite, Filter, funext, pow_one, iff_self
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.IsAsymptoticMulBasisOfOrder.mono line 148 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, LinearOrder, LocallyFiniteOrder, OrderBot, CanonicallyOrderedMul, IsCancelMul, LE.le, Set.IsAsymptoticMulBasisOfOrder
Proof uses: Finite, Infinite, Or, Eq, finite_or_infinite, Or.inl, of_eq_true, Or.inr, Membership.mem, Set.Nonempty, Set.IsAsymptoticMulBasisOfOrder.nonempty, HAdd.hAdd, Exists, Nat.exists_eq_add_of_le, Set.Finite.subset, Union.union, HSMul.hSMul, HPow.hPow, Compl.compl, Set.ofPred and 37 more
74 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_one_iff_Ioi line 175 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, LinearOrder, LocallyFiniteOrder, OrderBot, Iff, Set.IsAsymptoticMulBasisOfOrder, OfNat.ofNat, Nat, Exists, LE.le, Set.Ioi
Proof uses: of_eq_true, Eq.trans, LT.lt, Membership.mem, True, congr, congrArg, Filter.Eventually, HPow.hPow, Filter.cofinite, And, congrFun', Filter, funext, pow_one, propext, Filter.HasBasis.eventually_iff, Filter.cofinite_hasBasis_Ioi, forall_congr, implies_congr and 3 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_one_iff_Ici line 186 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, LinearOrder, LocallyFiniteOrder, OrderBot, SuccOrder, NoMaxOrder, Iff, Set.IsAsymptoticMulBasisOfOrder, OfNat.ofNat, Nat, Exists, LE.le, Set.Ici
Proof uses: of_eq_true, Eq.trans, Membership.mem, True, congr, congrArg, Filter.Eventually, HPow.hPow, Filter.cofinite, And, congrFun', Filter, funext, pow_one, propext, Filter.HasBasis.eventually_iff, Filter.cofinite_hasBasis_Ici, forall_congr, implies_congr, Eq.refl and 2 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_iff_atTop line 191 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, LinearOrder, LocallyFiniteOrder, OrderBot, SuccOrder, NoMaxOrder, Iff, Set.IsAsymptoticMulBasisOfOrder, Filter.Eventually, Membership.mem, HPow.hPow, Filter.atTop
Proof uses: Eq.mpr, Filter.cofinite, id, Eq, congrArg, Set.IsAsymptoticMulBasisOfOrder.eq_1, Filter, Filter.cofinite_eq_atTop, Iff.rfl
30 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma Set.isAsymptoticMulBasisOfOrder_iff_prod_atTop line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommMonoid, Set, Nat, LinearOrder, LocallyFiniteOrder, OrderBot, SuccOrder, NoMaxOrder, Iff, Set.IsAsymptoticMulBasisOfOrder, Filter.Eventually, Exists, Fin, And, Membership.mem, Eq, Finset.prod, Finset.univ, Filter.atTop
Proof uses: of_eq_true, Eq.trans, LE.le, True, congr, congrArg, Filter.cofinite, Filter, funext, Filter.cofinite_eq_atTop, iff_self
25 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
def Set.IsWeakMulBasisOfOrder line 208 source
no axioms what this means
Statement uses: CommMonoid, Set, Nat
Proof uses: Exists, And, LE.le, Membership.mem, HPow.hPow
9 instances, coercions and auxiliary constants left out.
def Set.IsWeakMulBasis A weak additive basis of some order line 212 source
Source documentation
A weak additive basis of some order.

no axioms what this means
Statement uses: CommMonoid, Set
Proof uses: Exists, Nat, Set.IsWeakMulBasisOfOrder
```
def IsWeakMulBasis (A : Set M) : Prop := ∃ n, A.IsWeakMulBasisOfOrder n
…
```