Commit 2025-08-13 09:52 da81383b

View on Github →

chore(RingTheory): use extend instead of abbrev in IsS(emis)impleModule (#27427)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Simple.lean

modified theorem simple_iff_isSimpleModule

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/LinearAlgebra/RootSystem/Irreducible.lean

Modified Mathlib/LinearAlgebra/Semisimple.lean

Modified Mathlib/RepresentationTheory/Maschke.lean

Modified Mathlib/RingTheory/Length.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

modified theorem IsSemisimpleModule.congr

modified theorem IsSimpleModule.congr

modified theorem RingEquiv.isSemisimpleRing

Modified Mathlib/RingTheory/SimpleModule/Rank.lean