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

13 declarations, 0 contain sorry, 0 declared as axioms

Fixed points of actions

We define types representing fixed points of actions on types, and define inherited typeclasses on these fixed point types. For example the fixed points of an action on an additive group is an additive group.

Main definitions

Given types M and A, with [SMul M A],

MulAction.FixedPoints M A is the subtype of A consisting of the a such that ∀ m, m • a = a.

Similarly, with [VAdd M A],

AddAction.FixedPoints M A is the subtype of A consisting of the a satisfying the unlikely-looking equation ∀ m, m +ᵥ a = a.

Notes

Note that the type MulAction.FixedPoints is the coercion to a type of the term MulAction.fixedPoints (which, presumably for historical reasons, is defined under a spurious extra hypothesis that M is a monoid). The motivation for this file is that using ↥fixedPoints can lead typeclass inference on a wild goose chase.

Imports (3)

Imported by 1 file

FLT.lean

def MulAction.FixedPoints If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M line 42 source
Source documentation
If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M.

no axioms what this means
Statement uses: SMul
Proof uses: Subtype, Eq, HSMul.hSMul
1 instances, coercions and auxiliary constants left out.
```
def MulAction.FixedPoints (M A : Type*) [SMul M A] : Type _ :=
…
```
def AddAction.FixedPoints If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M line 47 source
Source documentation
If M acts on A then FixedPoints M A is the type of elements of A which are fixed elementwise by all of M.

no axioms what this means
Statement uses: VAdd
Proof uses: Subtype, Eq, HVAdd.hVAdd
1 instances, coercions and auxiliary constants left out.
```
def AddAction.FixedPoints (M A : Type*) [VAdd M A] : Type _ :=
…
```
lemma MulAction.FixedPoints.ext line 57 source
no axioms what this means
Statement uses: SMul, MulAction.FixedPoints, Eq, HSMul.hSMul
Proof uses: Subtype, Subtype.mk, Eq.refl, Eq.symm
6 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
instance MulAction.FixedPoints.(instance at line 62) line 62 source
Source comment
TODO: don't know what I'm doing but Coe doesn't work because of semioutparam
```
instance [SMul M A] : CoeHead (FixedPoints M A) A where
…
```
Mentions: MulAction.FixedPoints
instance MulAction.FixedPoints.addZeroClass line 65 source
no axioms what this means
Statement uses: AddZeroClass, DistribSMul, MulAction.FixedPoints
Proof uses: AddZeroClass.mk, Zero.mk, Subtype.mk, Eq, HSMul.hSMul, OfNat.ofNat, Add.mk, HAdd.hAdd
17 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
lemma MulAction.FixedPoints.zero_def line 76 source
no axioms what this means
Statement uses: AddZeroClass, DistribSMul, Eq, MulAction.FixedPoints, OfNat.ofNat, Subtype.mk, HSMul.hSMul, smul_zero
Proof uses: rfl
13 instances, coercions and auxiliary constants left out.
lemma MulAction.FixedPoints.coe_add line 78 source
no axioms what this means
Statement uses: AddZeroClass, DistribSMul, MulAction.FixedPoints, Eq, HSMul.hSMul, HAdd.hAdd
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
instance MulAction.FixedPoints.addMonoid TODO: I could use FixedPoints.addSubmonoid + coercion to addMonoid, but Is my nsmul better? line 83 source
Source comment
TODO: I could use FixedPoints.addSubmonoid + coercion to addMonoid, but Is my `nsmul` better?

standard axioms: propext what this means
Statement uses: AddMonoid, DistribSMul, MulAction.FixedPoints
Proof uses: AddZeroClass, AddMonoid.mk, AddZeroClass.toZero, AddZeroClass.toAdd, NSMul.mk, Nat, Subtype.mk, Eq, HSMul.hSMul, NSMul.nsmul
20 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
instance addMonoid [AddMonoid A] [DistribSMul M A] : AddMonoid (FixedPoints M A) where
…
```
Mentions: MulAction.FixedPoints
instance MulAction.FixedPoints.addCommMonoid line 102 source
standard axioms: propext what this means
Statement uses: AddCommMonoid, DistribSMul, MulAction.FixedPoints
Proof uses: AddMonoid, AddCommMonoid.mk
14 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem MulAction.FixedPoints.smul_neg should be in mathlib; current version assumes M a monoid but same proof line 109 source
Source comment
should be in mathlib; current version assumes M a monoid but same proof

standard axioms: propext what this means
Statement uses: AddGroup, DistribSMul, Eq, HSMul.hSMul, Neg.neg
Proof uses: eq_neg_of_add_eq_zero_left, Eq.mpr, HAdd.hAdd, OfNat.ofNat, id, congrArg, Eq.symm, smul_add, neg_add_cancel, smul_zero, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem smul_neg [AddGroup A] [DistribSMul M A] (r : M) (x : A) : r • -x = -(r • x) :=
…
```
instance MulAction.FixedPoints.addGroup line 113 source
standard axioms: propext what this means
Statement uses: AddGroup, DistribSMul, MulAction.FixedPoints
Proof uses: AddMonoid, AddGroup.mk, SubNegMonoid.mk, Neg.mk, Subtype.mk, Eq, HSMul.hSMul, Neg.neg, Sub.mk, SubNegMonoid.sub', ZSMul.mk, Int, ZSMul.zsmul, Nat
29 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
instance MulAction.FixedPoints.addCommGroup line 139 source
standard axioms: propext what this means
Statement uses: AddCommGroup, DistribSMul, MulAction.FixedPoints
Proof uses: AddGroup, AddCommGroup.mk
18 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
instance MulAction.FixedPoints.module line 146 source
standard axioms: propext what this means
Statement uses: CommRing, AddCommGroup, Module, DistribSMul, SMulCommClass, MulAction.FixedPoints
Proof uses: Module.mk, DistribMulAction.mk, MulAction.mk, SemigroupAction.mk, SMul.mk, Subtype.mk, Eq, HSMul.hSMul
42 instances, coercions and auxiliary constants left out.

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