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

29 declarations, 6 contain sorry, 0 declared as axioms

Köthe conjecture

Reference: Wikipedia

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100OpenSet1.lean

def Koethe.IsNil Say a subset I of a ring R is nilpotent if all its elements are nilpotent line 41 source
Source documentation
Say a subset I of a ring R is nilpotent if all its elements are nilpotent.

no axioms what this means
Statement uses: Ring, SetLike
Proof uses: Membership.mem, IsNilpotent
7 instances, coercions and auxiliary constants left out.
```
def IsNil {S : Type*} [SetLike S R] (I : S) := ∀ i ∈ I, IsNilpotent i
…
```
def Koethe.KotheRadical The Kothe Radical of a ring R is the sum of all (two-sided) nil ideals of R line 48 source
Source documentation
The Kothe Radical of a ring R is the sum of all (two-sided) nil ideals of R. Tags: Kothe Radical, upper nilradical

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal
Proof uses: SupSet.sSup, Set.ofPred, Koethe.IsNil
6 instances, coercions and auxiliary constants left out.
```
def KotheRadical : TwoSidedIdeal R := sSup {I : TwoSidedIdeal R | IsNil I}
…
```
Mentions: Koethe.IsNil
theorem Koethe.IsNil.mono A subset of a nil subset is nil line 57 source
Source documentation
A subset of a nil subset is nil.

no axioms what this means
Statement uses: Ring, SetLike, LE.le, Set, Koethe.IsNil
Proof uses: Membership.mem
5 instances, coercions and auxiliary constants left out.
```
theorem IsNil.mono {S : Type*} [SetLike S R] {I J : S} (h : (I : Set R) ⊆ J) (hJ : IsNil J) :
    IsNil I :=
…
```
Mentions: Koethe.IsNil
theorem Koethe.isNil_bot The zero two-sided ideal is nil line 63 source
Source documentation
The zero two-sided ideal is nil.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, Koethe.IsNil, TwoSidedIdeal, Bot.bot
Proof uses: Membership.mem, Eq.rec, OfNat.ofNat, Eq, IsNilpotent, IsNilpotent.zero, Eq.symm, Eq.mp, congrArg, propext, TwoSidedIdeal.mem_bot
19 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_bot : IsNil (⊥ : TwoSidedIdeal R) := fun x hx => by
…
```
Mentions: Koethe.IsNil
theorem Koethe.IsNil.sup The sum of two nil two-sided ideals is nil line 69 source
Source documentation
The sum of two nil two-sided ideals is nil.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Max.max
Proof uses: Membership.mem, And, Exists, Eq, HAdd.hAdd, IsNilpotent, Iff.mp, TwoSidedIdeal.mem_sup, Nat, HPow.hPow, OfNat.ofNat, RingCon.Quotient, TwoSidedIdeal.ringCon, Iff.mpr, RingCon, RingCon.eq, Eq.mpr, id, congrArg, propext and 9 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem IsNil.sup {I J : TwoSidedIdeal R} (hI : IsNil I) (hJ : IsNil J) : IsNil (I ⊔ J) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.isNil_kotheRadical The Köthe radical is a nil ideal: every element of Nil* R is nilpotent line 85 source
Source documentation
The Köthe radical is a nil ideal: every element of Nil* R is nilpotent. This is a standard fact which does not depend on the Köthe conjecture.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, Koethe.IsNil, TwoSidedIdeal, Koethe.KotheRadical
Proof uses: TwoSidedIdeal.mk', Set.ofPred, Exists, And, Membership.mem, Exists.intro, OfNat.ofNat, Bot.bot, And.intro, Koethe.isNil_bot, TwoSidedIdeal.zero_mem, Set, HAdd.hAdd, Max.max, Koethe.IsNil.sup, AddMemClass.add_mem, TwoSidedIdeal.mem_sup_left, TwoSidedIdeal.mem_sup_right, Neg.neg, NegMemClass.neg_mem and 11 more
47 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_kotheRadical : IsNil (Nil* R) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.IsNil.map_mulRight If L is a nil left ideal, then so is L * y for any y line 105 source
Source documentation
If L is a nil left ideal, then so is L * y for any y.

standard axioms: Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, Submodule, Submodule.map, RingHom.id, LinearMap.mulRight
Proof uses: Membership.mem, And, Eq, LinearMap, Exists, IsNilpotent, Iff.mp, Submodule.mem_map, Nat, HPow.hPow, HMul.hMul, OfNat.ofNat, Ideal.mul_mem_left, Exists.intro, HAdd.hAdd, Eq.mpr, id, congrArg, LinearMap.mulRight_apply, pow_succ and 6 more
53 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem IsNil.map_mulRight {L : Ideal R} (hL : IsNil L) (y : R) :
    IsNil (Submodule.map (LinearMap.mulRight R y) L) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotheConjecture The Köthe conjecture: In any ring, the sum of two nil left ideals is nil sorry line 115 source
Source documentation
The Köthe conjecture: In any ring, the sum of two nil left ideals is nil.

depends on sorry what this means
Statement uses: Ring, Ideal, Koethe.IsNil, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
13 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem KotheConjecture (I J : Ideal R) (hI : IsNil I) (hJ : IsNil J) : IsNil (I + J) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotherConjecture.variants.le_KotherRadical The Köthe conjecture: every left nil radical is contained in the Köthe radical sorry line 120 source
Source documentation
The Köthe conjecture: every left nil radical is contained in the Köthe radical.

depends on sorry what this means
Statement uses: Ring, Ideal, Koethe.IsNil, LE.le, Set, TwoSidedIdeal, Koethe.KotheRadical
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
19 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.le_KotherRadical {I : Ideal R} (hI : IsNil I) :
    (I : Set R) ⊆ KotheRadical R := by
…
```
Mentions: Koethe.IsNil, Koethe.KotheRadical
theorem Koethe.KotherConjecture.variants.general_matrix The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_n(I) is a nil ideal of the matrix ring M_n(R) sorry line 128 source
Source documentation
The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_n(I) is a nil ideal of the matrix ring M_n(R).

depends on sorry what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Fintype, Matrix, Classical.propDecidable, Eq, TwoSidedIdeal.matrix
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
11 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.general_matrix {I : TwoSidedIdeal R} (hI : IsNil I)
    (n : Type*) [Fintype n] : IsNil (matrix n I) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotherConjecture.variants.two_by_two_matrix The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_2(I) is a nil ideal of the matrix ring M_2(R) sorry line 135 source
Source documentation
The Köthe conjecture: for any nil ideal I of R, the matrix ideal M_2(I) is a nil ideal of the matrix ring M_2(R).

depends on sorry what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Matrix, Fin, OfNat.ofNat, Nat, TwoSidedIdeal.matrix
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.two_by_two_matrix {I : TwoSidedIdeal R} (hI : IsNil I) :
    IsNil (matrix (Fin 2) I) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotherConjecture.variants.matrixOver_KotherRadical The Köthe conjecture: for any finite index type n, the Köthe radical of the matrix ring M_n(R) is the ideal M_n(Nil*(R)) of matrices with entries in the Köthe radical of R sorry line 143 source
Source documentation
The Köthe conjecture: for any finite index type n, the Köthe radical of the matrix ring M_n(R) is the ideal M_n(Nil*(R)) of matrices with entries in the Köthe radical of R.

depends on sorry what this means
Statement uses: Ring, Fintype, Eq, TwoSidedIdeal, Matrix, TwoSidedIdeal.matrix, Koethe.KotheRadical, Classical.propDecidable
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
9 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.matrixOver_KotherRadical (n : Type*) [Fintype n] :
    matrix n (Nil* R) = Nil* (Matrix n n R) := by
…
```
def Koethe.columnIdeal The left ideal of Matrix n n R consisting of the matrices with entries in I which are supported on the j-th column line 168 source
Source documentation
The left ideal of Matrix n n R consisting of the matrices with entries in I which are supported on the j-th column.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, TwoSidedIdeal, Ideal, Matrix
Proof uses: Submodule.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, And, Membership.mem, Ne, Eq, OfNat.ofNat, Set
23 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
def columnIdeal (I : TwoSidedIdeal R) (j : n) : Ideal (Matrix n n R) where
…
```
theorem Koethe.pow_succ_apply_of_mem_columnIdeal Powers of a matrix supported on the j-th column are controlled by the (j, j) entry line 180 source
Source documentation
Powers of a matrix supported on the j-th column are controlled by the (j, j) entry.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, TwoSidedIdeal, Matrix, Membership.mem, Ideal, Koethe.columnIdeal, Nat, Eq, HPow.hPow, HAdd.hAdd, OfNat.ofNat, HMul.hMul
Proof uses: Nat.recAux, of_eq_true, Eq.trans, True, congr, congrArg, congrFun', zero_add, pow_one, pow_zero, mul_one, eq_self, Eq.mpr, id, pow_succ, Finset.sum, Finset.univ, Matrix.mul_apply, Ne, Or and 12 more
63 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
theorem pow_succ_apply_of_mem_columnIdeal {I : TwoSidedIdeal R} {j : n} {M : Matrix n n R}
    (hM : M ∈ columnIdeal I j) (m : ℕ) (i k : n) :
    (M ^ (m + 1)) i k = M i k * M j j ^ m := by
…
```
Mentions: Koethe.columnIdeal
theorem Koethe.isNil_columnIdeal For a nil ideal I, the column ideals columnIdeal I j are nil left ideals line 195 source
Source documentation
For a nil ideal I, the column ideals columnIdeal I j are nil left ideals.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, TwoSidedIdeal, Koethe.IsNil, Matrix, Ideal, Koethe.columnIdeal
Proof uses: Membership.mem, Nat, Eq, HPow.hPow, OfNat.ofNat, IsNilpotent, And.left, Ne, Exists.intro, HAdd.hAdd, Matrix.ext, Eq.mpr, HMul.hMul, id, congrArg, Koethe.pow_succ_apply_of_mem_columnIdeal, MulZeroClass.mul_zero, Matrix.zero_apply, Eq.refl
42 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_columnIdeal {I : TwoSidedIdeal R} (hI : IsNil I) (j : n) :
    IsNil (columnIdeal I j) := by
…
```
Mentions: Koethe.IsNil, Koethe.columnIdeal
theorem Koethe.mem_iSup_columnIdeal The matrix ideal M_n(I) is the sum of the column ideals columnIdeal I j line 205 source
Source documentation
The matrix ideal M_n(I) is the sum of the column ideals columnIdeal I j.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, TwoSidedIdeal, Matrix, Membership.mem, TwoSidedIdeal.matrix, Ideal, iSup, Koethe.columnIdeal
Proof uses: Eq, Finset.sum, Finset.univ, Equiv, Matrix.of, ite, OfNat.ofNat, Matrix.ext, of_eq_true, Eq.trans, True, congrArg, Matrix.sum_apply, Finset, Finset.sum_ite_eq, ite_cond_eq_true, eq_self, Eq.mpr, id, sum_mem and 9 more
41 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem mem_iSup_columnIdeal {I : TwoSidedIdeal R} {M : Matrix n n R}
    (hM : M ∈ TwoSidedIdeal.matrix n I) :
    M ∈ ⨆ j, columnIdeal I j := by
…
```
Mentions: Koethe.columnIdeal
theorem Koethe.isNil_iSup_of_kotheConjecture If the Köthe conjecture holds (for rings in universe w), then a finite sum of nil left ideals is nil line 224 source
Source documentation
If the Köthe conjecture holds (for rings in universe w), then a finite sum of nil left ideals is nil.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, HAdd.hAdd, Fintype, iSup
Proof uses: Eq.mpr, Finset.sup, Finset.univ, id, Eq, congrArg, Eq.symm, Finset.sup_univ_eq_iSup, Finset.sup_induction, Membership.mem, Bot.bot, Eq.rec, OfNat.ofNat, IsNilpotent, IsNilpotent.zero, Eq.mp, Submodule, propext, Submodule.mem_bot, Finset
42 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_iSup_of_kotheConjecture (h : type_of% @KotheConjecture.{w}) {S : Type w} [Ring S]
    {ι : Type*} [Fintype ι] {L : ι → Ideal S} (hL : ∀ i, IsNil (L i)) :
    IsNil (⨆ i, L i) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotherConjecture.variants.general_matrix_of_KotheConjecture The Köthe conjecture (for rings in universe max u v) implies the general matrix formulation for rings in universe u and index types in universe v line 236 source
Source documentation
The Köthe conjecture (for rings in universe max u v) implies the general matrix formulation for rings in universe u and index types in universe v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, HAdd.hAdd, TwoSidedIdeal, Fintype, Matrix, Classical.propDecidable, Eq, TwoSidedIdeal.matrix
Proof uses: Membership.mem, Koethe.isNil_iSup_of_kotheConjecture, Koethe.columnIdeal, Koethe.isNil_columnIdeal, Koethe.mem_iSup_columnIdeal
23 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.general_matrix_of_KotheConjecture
    (h : type_of% @KotheConjecture.{max u v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v} := by
…
```
theorem Koethe.KotherConjecture.variants.KotheConjecture_of_le_KotherRadical If every nil left ideal is contained in the Köthe radical, then the Köthe conjecture holds line 246 source
Source documentation
If every nil left ideal is contained in the Köthe radical, then the Köthe conjecture holds.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, LE.le, Set, TwoSidedIdeal, Koethe.KotheRadical, HAdd.hAdd
Proof uses: Membership.mem, And, Submodule, Exists, Eq, IsNilpotent, Eq.mp, Max.max, congrArg, propext, Submodule.mem_sup, Submodule.add_eq_sup, Koethe.isNil_kotheRadical, AddMemClass.add_mem
47 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.KotheConjecture_of_le_KotherRadical
    (h : type_of% @KotherConjecture.variants.le_KotherRadical.{u}) :
    type_of% @KotheConjecture.{u} := by
…
```
theorem Koethe.KotherConjecture.variants.le_KotherRadical_of_KotheConjecture The Köthe conjecture implies that every nil left ideal is contained in the Köthe radical line 256 source
Source documentation
The Köthe conjecture implies that every nil left ideal is contained in the Köthe radical.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, HAdd.hAdd, LE.le, Set, TwoSidedIdeal, Koethe.KotheRadical
Proof uses: TwoSidedIdeal.mk', Set.ofPred, Exists, And, Membership.mem, Exists.intro, OfNat.ofNat, Bot.bot, And.intro, Eq.rec, Eq, IsNilpotent, IsNilpotent.zero, Eq.symm, Eq.mp, congrArg, propext, Ideal.mem_bot, Submodule.zero_mem, Submodule.add_mem_sup and 15 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.le_KotherRadical_of_KotheConjecture
    (h : type_of% @KotheConjecture.{u}) :
    type_of% @KotherConjecture.variants.le_KotherRadical.{u} := by
…
```
theorem Koethe.KotherConjecture.variants.general_matrix_of_le_KotherRadical If every nil left ideal is contained in the Köthe radical (for rings in universe max u v), then the general matrix formulation holds line 283 source
Source documentation
If every nil left ideal is contained in the Köthe radical (for rings in universe max u v), then the general matrix formulation holds.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Ideal, Koethe.IsNil, LE.le, Set, TwoSidedIdeal, Koethe.KotheRadical, Fintype, Matrix, Classical.propDecidable, Eq, TwoSidedIdeal.matrix
Proof uses: Koethe.KotherConjecture.variants.general_matrix_of_KotheConjecture, Koethe.KotherConjecture.variants.KotheConjecture_of_le_KotherRadical
20 instances, coercions and auxiliary constants left out.
```
theorem KotherConjecture.variants.general_matrix_of_le_KotherRadical
    (h : type_of% @KotherConjecture.variants.le_KotherRadical.{max u v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v} :=
…
```
theorem Koethe.KotherConjecture.variants.two_by_two_matrix_of_general_matrix The general matrix formulation of the Köthe conjecture trivially implies the 2 × 2 one line 290 source
Source documentation
The general matrix formulation of the Köthe conjecture trivially implies the 2 × 2 one.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Fintype, Matrix, Classical.propDecidable, Eq, TwoSidedIdeal.matrix, Fin, OfNat.ofNat, Nat
Proof uses: Eq.mpr, eq_of_heq, SetLike, HEq, Eq.refl, HEq.refl, Eq.symm, DecidableEq, Lean.Meta.FastSubsingleton.elim, Decidable
20 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.two_by_two_matrix_of_general_matrix
    (h : type_of% @KotherConjecture.variants.general_matrix.{u, 0}) :
    type_of% @KotherConjecture.variants.two_by_two_matrix.{u} := by
…
```
theorem Koethe.isNil_matrix_of_equiv Nilness of the matrix ideal M_n(I) only depends on the cardinality of n line 302 source
Source documentation
Nilness of the matrix ideal M_n(I) only depends on the cardinality of n.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, Equiv, TwoSidedIdeal, Koethe.IsNil, Matrix, TwoSidedIdeal.matrix
Proof uses: Membership.mem, RingEquiv, RingEquiv.symm, Matrix.reindexRingEquiv, Eq.mp, IsNilpotent, congrArg, Eq.trans, Matrix.submatrix, Equiv.symm, Function.comp, Matrix.submatrix_submatrix, id, congr, Equiv.self_comp_symm, Matrix.submatrix_id_id, IsNilpotent.map
37 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_matrix_of_equiv (e : m ≃ n) {I : TwoSidedIdeal R}
    (h : IsNil (TwoSidedIdeal.matrix m I)) : IsNil (TwoSidedIdeal.matrix n I) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.isNil_matrix_of_sum If M_{n ⊕ m}(I) is nil then so is M_n(I), using the block embedding line 310 source
Source documentation
If M_{n ⊕ m}(I) is nil then so is M_n(I), using the block embedding.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, DecidableEq, TwoSidedIdeal, Koethe.IsNil, Matrix, Sum, TwoSidedIdeal.matrix
Proof uses: Membership.mem, Matrix.fromBlocks, OfNat.ofNat, Eq.mpr, id, Eq, congrArg, propext, TwoSidedIdeal.mem_matrix, Sum.inl, of_eq_true, eq_true, Eq.mp, Sum.inr, Nat, HPow.hPow, IsNilpotent, HAdd.hAdd, Nat.recAux, Eq.trans and 21 more
59 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_matrix_of_sum {I : TwoSidedIdeal R} (h : IsNil (TwoSidedIdeal.matrix (n ⊕ m) I)) :
    IsNil (TwoSidedIdeal.matrix n I) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.isNil_matrix_prod_of_two_by_two_matrix If M_2(J) is nil for every nil ideal J of every ring in universe u, then nilness of M_m(I) implies nilness of M_{2m}(I), using M_2(M_m(R)) ≃ M_{2m}(R) line 332 source
Source documentation
If M_2(J) is nil for every nil ideal J of every ring in universe u, then nilness of M_m(I) implies nilness of M_{2m}(I), using M_2(M_m(R)) ≃ M_{2m}(R).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Matrix, Fin, OfNat.ofNat, Nat, TwoSidedIdeal.matrix, Fintype, DecidableEq, Prod
Proof uses: Membership.mem, RingEquiv, RingEquiv.symm, Matrix.compRingEquiv, Prod.mk, Eq.mp, IsNilpotent, congrArg, Equiv.apply_symm_apply, Matrix.comp, IsNilpotent.map
47 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem isNil_matrix_prod_of_two_by_two_matrix
    (h : type_of% @KotherConjecture.variants.two_by_two_matrix.{u}) {R : Type u} [Ring R]
    {m : Type} [Fintype m] [DecidableEq m] {I : TwoSidedIdeal R}
    (hm : IsNil (TwoSidedIdeal.matrix m I)) : IsNil (TwoSidedIdeal.matrix (Fin 2 × m) I) := by
…
```
Mentions: Koethe.IsNil
theorem Koethe.KotherConjecture.variants.general_matrix_of_two_by_two_matrix Documented declaration: general_matrix_of_two_by_two_matrix line 346 source
Source documentation
The 2 × 2 matrix formulation of the Köthe conjecture (for rings in universe u) implies the general matrix formulation (Krempa): one first deduces the case of 2 ^ k × 2 ^ k matrices by induction and then embeds M_n(R) in a corner of M_{2 ^ k}(R).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Matrix, Fin, OfNat.ofNat, Nat, TwoSidedIdeal.matrix, Fintype, Classical.propDecidable, Eq
Proof uses: HAdd.hAdd, Nat.recAux, Koethe.isNil_matrix_of_equiv, Equiv.symm, Equiv.funUnique, Prod, Fin.consEquiv, Koethe.isNil_matrix_prod_of_two_by_two_matrix, LE.le, Fintype.card, HPow.hPow, LE.le.trans, LT.lt.le, Nat.lt_two_pow_self, Nat.pow_le_pow_right, two_pos, Nat.le_succ, Equiv, Sum, HSub.hSub and 20 more
51 instances, coercions and auxiliary constants left out.

Tactic trace: 12 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.general_matrix_of_two_by_two_matrix
    (h : type_of% @KotherConjecture.variants.two_by_two_matrix.{u}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v} := by
…
```
theorem Koethe.KotherConjecture.variants.general_matrix_of_matrixOver_KotherRadical The formulation of the Köthe conjecture in terms of the Köthe radical of matrix rings implies the general matrix formulation line 368 source
Source documentation
The formulation of the Köthe conjecture in terms of the Köthe radical of matrix rings implies the general matrix formulation.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, Fintype, Eq, TwoSidedIdeal, Matrix, TwoSidedIdeal.matrix, Koethe.KotheRadical, Classical.propDecidable, Koethe.IsNil
Proof uses: Koethe.IsNil.mono, Eq.mpr, LE.le, Set, id, congrArg, Eq.symm, Iff.mp, TwoSidedIdeal.le_iff, TwoSidedIdeal.matrix_monotone, le_sSup, Set.ofPred, Koethe.isNil_kotheRadical
16 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.general_matrix_of_matrixOver_KotherRadical
    (h : type_of% @KotherConjecture.variants.matrixOver_KotherRadical.{u, v}) :
    type_of% @KotherConjecture.variants.general_matrix.{u, v} := by
…
```
theorem Koethe.KotherConjecture.variants.matrixOver_KotherRadical_of_general_matrix The general matrix formulation of the Köthe conjecture implies the formulation in terms of the Köthe radical of matrix rings line 380 source
Source documentation
The general matrix formulation of the Köthe conjecture implies the formulation in terms of the Köthe radical of matrix rings.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Ring, TwoSidedIdeal, Koethe.IsNil, Fintype, Matrix, Classical.propDecidable, Eq, TwoSidedIdeal.matrix, Koethe.KotheRadical
Proof uses: le_antisymm, le_sSup, Set.ofPred, Koethe.isNil_kotheRadical, Membership.mem, Nonempty, Nonempty.intro, Exists, RingCon, TwoSidedIdeal.ringCon, OfNat.ofNat, Exists.intro, Equiv, Equiv.symm, TwoSidedIdeal.equivMatrix, Eq.symm, Equiv.apply_symm_apply, Matrix.single, Eq.mpr, id and 34 more
57 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
theorem KotherConjecture.variants.matrixOver_KotherRadical_of_general_matrix
    (h : type_of% @KotherConjecture.variants.general_matrix.{u, v}) :
    type_of% @KotherConjecture.variants.matrixOver_KotherRadical.{u, v} := by
…
```
theorem Koethe.amitsur_conjecture The Amitsur Conjecture: If J is a nil ideal in R, then J[x] is a nil ideal of the polynomial ring R[x] sorry line 426 source
Source documentation
The Amitsur Conjecture: If J is a nil ideal in R, then J[x] is a nil ideal of the polynomial ring R[x]. This is known to be false, see Agata Smoktunowicz, Polynomial rings over nil rings need not be nil.

depends on sorry what this means
Statement uses: Not, Ring, TwoSidedIdeal, Koethe.IsNil, Polynomial, TwoSidedIdeal.map, RingHom, Polynomial.C
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
17 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem amitsur_conjecture : ¬ ∀ (R : Type) [Ring R] (J : TwoSidedIdeal R), IsNil J →
    IsNil (TwoSidedIdeal.map (Polynomial.C) J) := by
…
```
Mentions: Koethe.IsNil