Commit 2024-04-08 18:06 8596db69

View on Github →

feat(RingTheory/Noetherian): characterise nilpotent endomorphisms of finitely-generated modules (#11926)

Estimated changes

Modified Mathlib/RingTheory/Finiteness.lean

added theorem Module.Finite.Module.End.isNilpotent_iff_of_finite