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

12 declarations, 0 contain sorry, 0 declared as axioms

Compatibility aliases for the original odd-representation namespace

The maintained proof of the odd-representation irreducibility criterion now lives in FLT.Slop.RepresentationTheory.OddAbsIrredSlop, under Slop.OddRep. This file keeps the old Slop.OddRepOrig names available without recompiling a duplicate copy of the same proofs.

Imports (1)

FLT.Slop.RepresentationTheory.OddAbsIrredSlop

Imported by 1 file

FLT.lean

abbrev Slop.OddRepOrig.baseChange Compatibility alias for Slop.OddRep.baseChange line 32 source
Source documentation
Compatibility alias for Slop.OddRep.baseChange.

standard axioms: Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Algebra, Representation, TensorProduct
Proof uses: Slop.OddRep.baseChange
14 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev baseChange (l : Type*) [Field l] [Algebra k l]
    (ρ : Representation k G V) : Representation l G (l ⊗[k] V) :=
…
```
abbrev Slop.OddRepOrig.adjoinRange Compatibility alias for Slop.OddRep.adjoinRange line 37 source
Source documentation
Compatibility alias for Slop.OddRep.adjoinRange.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Subalgebra, Module.End
Proof uses: Slop.OddRep.adjoinRange
22 instances, coercions and auxiliary constants left out.
```
abbrev adjoinRange (ρ : Representation k G V) : Subalgebra k (Module.End k V) :=
…
```
abbrev Slop.OddRepOrig.IsAbsolutelyIrreducible Compatibility alias for Slop.OddRep.IsAbsolutelyIrreducible line 41 source
Source documentation
Compatibility alias for Slop.OddRep.IsAbsolutelyIrreducible.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation
Proof uses: Slop.OddRep.IsAbsolutelyIrreducible
8 instances, coercions and auxiliary constants left out.
```
abbrev IsAbsolutelyIrreducible (ρ : Representation k G V) : Prop :=
…
```
lemma Slop.OddRepOrig.isIrreducible_iff_forall line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Iff, Representation.IsIrreducible, And, Nontrivial, Submodule, Membership.mem, LinearMap, RingHom.id, Or, Eq, Bot.bot, Top.top
Proof uses: Slop.OddRep.isIrreducible_iff_forall
21 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.smul_tmul_mem_range_iff line 50 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, AddCommGroup, Module, Algebra, Ne, OfNat.ofNat, Iff, Membership.mem, TensorProduct, Submodule, LinearMap.range, RingHom.id, LinearMap, TensorProduct.mk, TensorProduct.tmul, Exists, Eq, RingHom, Algebra.algebraMap
Proof uses: Slop.OddRep.smul_tmul_mem_range_iff
48 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.exists_smul_eq_of_commute line 56 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Representation.IsIrreducible, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, Module.End, Commute, Exists, HSMul.hSMul
Proof uses: Slop.OddRep.exists_smul_eq_of_commute
66 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.adjoinRange_eq_top line 64 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Representation.IsIrreducible, Module.End, Commute, LinearMap, RingHom.id, Exists, Eq, HSMul.hSMul, OfNat.ofNat, Subalgebra, Slop.OddRepOrig.adjoinRange, Top.top
Proof uses: Slop.OddRep.adjoinRange_eq_top
74 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.adjoinRange_baseChange_eq_top line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Algebra, Eq, Subalgebra, Module.End, Slop.OddRepOrig.adjoinRange, Top.top, TensorProduct, Slop.OddRepOrig.baseChange
Proof uses: Slop.OddRep.adjoinRange_baseChange_eq_top
64 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.isIrreducible_of_adjoinRange_eq_top line 77 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Nontrivial, Eq, Subalgebra, Module.End, Slop.OddRepOrig.adjoinRange, Top.top, Representation.IsIrreducible
Proof uses: Slop.OddRep.isIrreducible_of_adjoinRange_eq_top
54 instances, coercions and auxiliary constants left out.
lemma Slop.OddRepOrig.isIrreducible_of_baseChange line 82 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, Algebra, Representation.IsIrreducible, TensorProduct, Slop.OddRepOrig.baseChange
Proof uses: Slop.OddRep.isIrreducible_of_baseChange
26 instances, coercions and auxiliary constants left out.
theorem Slop.OddRepOrig.isIrreducible_baseChange_of_finrank_eigenspace_eq_one line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Algebra, Representation.IsIrreducible, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, TensorProduct, Slop.OddRepOrig.baseChange
Proof uses: Slop.OddRep.isIrreducible_baseChange_of_finrank_eigenspace_eq_one
57 instances, coercions and auxiliary constants left out.
theorem Slop.OddRepOrig.isIrreducible_iff_isAbsolutelyIrreducible line 96 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Monoid, AddCommGroup, Module, Representation, FiniteDimensional, Eq, Nat, Module.finrank, Subtype, Membership.mem, Submodule, Module.End.eigenspace, LinearMap, RingHom.id, OfNat.ofNat, Iff, Representation.IsIrreducible, Slop.OddRepOrig.IsAbsolutelyIrreducible
Proof uses: Slop.OddRep.isIrreducible_iff_isAbsolutelyIrreducible_slop
50 instances, coercions and auxiliary constants left out.