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

23 declarations, 0 contain sorry, 0 declared as axioms

Basic

Material destined for Mathlib.

Imports (5)

Imported by 6 files

def RestrictedProduct.mapAlongLinearMap Documented declaration: mapAlongLinearMap line 64 source
Source documentation
Given two restricted products Πʳ (i : ι₁), [R₁ i, B₁ i]_[𝓕₁] and Πʳ (j : ι₂), [R₂ j, B₂ j]_[𝓕₂] of A-modules, RestrictedProduct.mapAlongLinearMap gives an A-linear map between them. The data needed is a function f : ι₂ → ι₁ such that 𝓕₂ tends to 𝓕₁ along f, and A-linear maps φ j : R₁ (f j) → R₂ j sending B₁ (f j) into B₂ j for an 𝓕₂-large set of j's.

standard axioms: Quot.sound, propext what this means
Statement uses: Filter, SetLike, Filter.Tendsto, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, LinearMap, RingHom.id, Filter.Eventually, Set.MapsTo, RestrictedProduct
Proof uses: AddMonoidHom, RestrictedProduct.mapAlongAddMonoidHom, LinearMap.mk, AddHom.mk, ZeroHom.toFun
39 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
def RestrictedProduct.mapAlongLinearMap :
    Πʳ i, [R₁ i, B₁ i]_[𝓕₁] →ₗ[A] Πʳ j, [R₂ j, B₂ j]_[𝓕₂] where
…
```
lemma RestrictedProduct.mapAlongLinearMap_apply line 72 source
standard axioms: Quot.sound, propext what this means
Statement uses: Filter, SetLike, Filter.Tendsto, Semiring, AddCommMonoid, Module, AddSubmonoidClass, SMulMemClass, LinearMap, RingHom.id, Filter.Eventually, Set.MapsTo, RestrictedProduct, Eq, RestrictedProduct.mapAlongLinearMap
Proof uses: rfl
32 instances, coercions and auxiliary constants left out.
def RestrictedProduct.inclusionLinearMap Documented declaration: inclusionLinearMap line 84 source
Source documentation
A linear map version of RestrictedProduct.inclusion : if 𝓕 ≤ 𝓖 then there's a linear map Πʳ i, [R i, C i]_[𝓖] →ₗ[A] Πʳ i, [R i, C i]_[𝓕] where the R i are A-modules and the C i are submodules.

standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Filter, LE.le, LinearMap, RingHom.id, RestrictedProduct
Proof uses: RestrictedProduct.mapAlongLinearMap, id, LinearMap.id
23 instances, coercions and auxiliary constants left out.
```
def RestrictedProduct.inclusionLinearMap
     {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) :
    Πʳ i, [R i, C i]_[𝓖] →ₗ[A] Πʳ i, [R i, C i]_[𝓕] :=
…
```
lemma inclusionLinearMap_apply line 90 source
standard axioms: Quot.sound, propext what this means
Statement uses: CommRing, AddCommGroup, Module, Submodule, Filter, LE.le, RestrictedProduct, Eq, LinearMap, RingHom.id, RestrictedProduct.inclusionLinearMap, Subtype.mk, Filter.Eventually, Membership.mem, Set, Filter.Eventually.filter_mono, Subtype.property
Proof uses: rfl
32 instances, coercions and auxiliary constants left out.
def RestrictedProduct.mulSupport line 118 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, One, RestrictedProduct, Filter.cofinite, Set
Proof uses: Set.ofPred, Ne, OfNat.ofNat
5 instances, coercions and auxiliary constants left out.
lemma RestrictedProduct.not_mem_mulSupport line 123 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, One, RestrictedProduct, Filter.cofinite, Iff, Not, Membership.mem, Set, RestrictedProduct.mulSupport, Eq, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, iff_self
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.mul_comm_of_disjoint_mulSupport line 128 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Monoid, SubmonoidClass, RestrictedProduct, Filter.cofinite, Eq, Set, Inter.inter, RestrictedProduct.mulSupport, EmptyCollection.emptyCollection, HMul.hMul
Proof uses: RestrictedProduct.ext, Not, Membership.mem, Or, And, Iff.mp, Iff, Decidable.iff_iff_and_or_not_and_not, Eq.mp, congrArg, propext, Set.ext_iff, False.elim, False, Iff.mpr, Classical.or_iff_not_imp_left, And.intro, Decidable.of_not_not, Classical.propDecidable, of_eq_true and 9 more
28 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.mulSupport_mul_subset line 142 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Monoid, SubmonoidClass, RestrictedProduct, Filter.cofinite, Set, LE.le, RestrictedProduct.mulSupport, HMul.hMul
Proof uses: Membership.mem, Mathlib.Tactic.Contrapose.contrapose₁, Not, of_eq_true, Eq.trans, Eq, OfNat.ofNat, True, congrFun', congrArg, congr, Iff.mp, RestrictedProduct.not_mem_mulSupport, mul_one, eq_self
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.mulSupport_inv line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Group, SubgroupClass, RestrictedProduct, Filter.cofinite, Eq, Set, RestrictedProduct.mulSupport, Inv.inv
Proof uses: Set.ext, id, Iff, Membership.mem, inv_ne_one
21 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.SubmonoidClass.isProductAt A submonoid U of a resticted product of monoids is a product at i if U can be written as Uᵢ × Uⁱ with Uᵢ supported at the i'th component and Uⁱ supported away from i line 163 source
Source documentation
A submonoid U of a resticted product of monoids is a product at i if U can be written as Uᵢ × Uⁱ with Uᵢ supported at the i'th component and Uⁱ supported away from i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Monoid, SubmonoidClass, RestrictedProduct, Filter.cofinite
Proof uses: Membership.mem, Exists, And, Eq, HMul.hMul, LE.le, Set, RestrictedProduct.mulSupport, Singleton.singleton, Not
14 instances, coercions and auxiliary constants left out.
```
def SubmonoidClass.isProductAt (U : T) (i : ι) : Prop :=
…
```
lemma RestrictedProduct.mem_coset_and_mulSupport_subset_of_isProductAt If U is a product at i and g is supported at i then UgU can be written as a disjoint union of cosets gᵢU with the gᵢ supported at i line 174 source
Source documentation
If U is a product at i and g is supported at i then UgU can be written as a disjoint union of cosets gᵢU with the gᵢ supported at i.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, Group, SubgroupClass, RestrictedProduct, Filter.cofinite, RestrictedProduct.SubmonoidClass.isProductAt, LE.le, Set, RestrictedProduct.mulSupport, Singleton.singleton, Membership.mem, HMul.hMul, Set.mul, HSMul.hSMul, Set.smulSet, Exists, And
Proof uses: Eq, Not, Exists.intro, And.intro, Inv.inv, MulMemClass.mul_mem, InvMemClass.inv_mem, RestrictedProduct.mul_comm_of_disjoint_mulSupport, Eq.mpr, Inter.inter, EmptyCollection.emptyCollection, id, congrArg, RestrictedProduct.mulSupport_inv, propext, Set.eq_empty_iff_forall_notMem, False, Eq.mp, of_eq_true, Eq.trans and 7 more
56 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma mem_coset_and_mulSupport_subset_of_isProductAt
    {U : T} (i : ι) (g : Πʳ i, [G i, A i])
    (hU : SubmonoidClass.isProductAt U i) (hg : mulSupport g ⊆ {i}) (γ : Πʳ i, [G i, A i])
    (hγ : γ ∈ U * g • (U : Set (Πʳ i, [G i, A i]))) :
    ∃ δ, δ ∈ γ • (U : Set (Πʳ i, [G i, A i])) ∧ mulSupport δ ⊆ {i} := by
…
```
Mentions: RestrictedProduct.SubmonoidClass.isProductAt, RestrictedProduct.mulSupport
def RestrictedProduct.indexSupport line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, RestrictedProduct, Filter.cofinite, Finset
Proof uses: Set.Finite.toFinset, Set.ofPred, Not, Membership.mem
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem RestrictedProduct.mem_indexSupport_iff line 200 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: SetLike, RestrictedProduct, Filter.cofinite, Iff, Membership.mem, Finset, RestrictedProduct.indexSupport, Not
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Set.ofPred, 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 RestrictedProduct.components_comp_coe_eq_coe_apply line 216 source
standard axioms: Quot.sound, propext what this means
Statement uses: Filter, Set, RestrictedProduct, Eq, Function.comp
Proof uses: funext, of_eq_true, Eq.trans, True, congrArg, eq_self
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.exists_update line 220 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, RestrictedProduct, Membership.mem, Compl.compl, Singleton.singleton, Exists, And, Eq, Ne
Proof uses: Exists.intro, Subtype.mk, Filter.Eventually, dite, Classical.propDecidable, Eq.rec, Eq.symm, Not, Filter.mp_mem, Set.ofPred, Subtype.property, Filter.univ_mem', id, Eq.mpr, congrArg, dite_eq_right_of_eq_false, eq_false, of_eq_true, Eq.trans, True and 15 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.exists_apply_eq line 229 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Nonempty, Membership.mem, Compl.compl, Singleton.singleton, Exists, RestrictedProduct, Eq
Proof uses: Subtype.mk, Filter.Eventually, Classical.ofNonempty, Filter.Eventually.of_forall, Subtype.coe_prop, And, Ne, RestrictedProduct.exists_update, Exists.intro
16 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.surjective_components_of_surjective line 239 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, RestrictedProduct, Eq, Nonempty, Function.Surjective, Membership.mem, Compl.compl, Singleton.singleton
Proof uses: Exists, RestrictedProduct.exists_apply_eq, Exists.intro, Eq.mpr, id, congrArg, Eq.symm, Eq.refl
13 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma RestrictedProduct.eventually_surjOn_of_surjective line 248 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, Set, Eq, Filter.comap, RestrictedProduct, Nonempty, Function.Surjective, Filter.Eventually, Set.SurjOn
Proof uses: Exists, Membership.mem, dite, Classical.propDecidable, Exists.intro, Classical.choice, inferInstance, Not, And, Set.image, Eq.mp, LE.le, congrArg, propext, Set.not_subset_iff_exists_mem_notMem, Set.SurjOn.eq_1, Subtype.mk, absurd, And.intro, Filter.Eventually.of_forall and 15 more
13 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.structureMapMonoidHom line 276 source
standard axioms: Quot.sound what this means
Statement uses: Monoid, SetLike, SubmonoidClass, Filter, MonoidHom, Subtype, Membership.mem, RestrictedProduct, Submonoid, Submonoid.ofClass
Proof uses: MonoidHom.mk, OneHom.mk, RestrictedProduct.structureMap
21 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
def RestrictedProduct.structureMapRingHom The structure map for a restricted product of ring line 284 source
Source documentation
The structure map for a restricted product of ring.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, Filter, RingHom, Subtype, Membership.mem, RestrictedProduct, Subring, Subring.ofClass
Proof uses: RingHom.mk, MonoidHom.mk, OneHom.mk, RestrictedProduct.structureMap
28 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
def structureMapRingHom {ι : Type*} (M : ι → Type*) [(i : ι) → Ring (M i)]
    {S : ι → Type*} [∀ i, SetLike (S i) (M i)] [∀ i, SubringClass (S i) (M i)] (A : Π i, S i)
    (𝓕 : Filter ι) : ((i : ι) → (A i)) →+* Πʳ (i : ι), [M i, Subring.ofClass (A i)]_[𝓕] where
…
```
lemma RestrictedProduct.structureMapRingHom_apply_apply line 294 source
standard axioms: Quot.sound, propext what this means
Statement uses: Ring, SetLike, SubringClass, Filter, Subtype, Membership.mem, Eq, RestrictedProduct, Subring, Subring.ofClass, RingHom, RestrictedProduct.structureMapRingHom
Proof uses: rfl
27 instances, coercions and auxiliary constants left out.
def RestrictedProduct.structureSubring The subring ∏ i, A i inside Πʳ i, [R i, A i]_[𝓕] line 299 source
Source documentation
The subring ∏ i, A i inside Πʳ i, [R i, A i]_[𝓕].

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, SetLike, Ring, SubringClass, Subring, RestrictedProduct
Proof uses: RingHom.range, Subtype, Membership.mem, Subring.ofClass, RestrictedProduct.structureMapRingHom
11 instances, coercions and auxiliary constants left out.
```
def structureSubring {ι : Type*} (R : ι → Type*) {S : ι → Type*}
    (A : (i : ι) → (S i)) (𝓕 : Filter ι) [(i : ι) → SetLike (S i) (R i)] [(i : ι) → Ring (R i)]
    [(i : ι) → SubringClass (S i) (R i)] :
    Subring (Πʳ i, [R i, A i]_[𝓕]) :=
…
```
theorem RestrictedProduct.mem_structureSubring_iff line 306 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Filter, SetLike, Ring, SubringClass, RestrictedProduct, Iff, Membership.mem, Subring, RestrictedProduct.structureSubring
Proof uses: Eq.mpr, RingHom.range, Subtype, Subring.ofClass, RestrictedProduct.structureMapRingHom, id, Eq, congrArg, RestrictedProduct.structureSubring.eq_1, Set, Set.range, RestrictedProduct.structureMap, Set.ofPred, Filter.Eventually, RestrictedProduct.range_structureMap, congrFun', funext, forall_congr, Iff.rfl
21 instances, coercions and auxiliary constants left out.

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