Theorems · Definition · ring theory
IsSemisimpleRing
(R : Type u_2) → [Ring R] → Prop
A ring is semisimple if it is semisimple as a module over itself.
- Defined in
- Mathlib.RingTheory.SimpleModule.Basic
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses no axioms
- Assumes
- Ring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- IsSemisimpleModuleproof · cited by 67
Cited by30
Results whose statement or proof uses this declaration.
- RingEquiv.isSemisimpleRingstatement and proof · cited by 6
- Module.End.isSemisimple_of_squarefree_aeval_eq_zeroproof · cited by 4
- IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRingstatement and proof · cited by 2
- IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOppositestatement and proof · cited by 2
- IsNoetherianRing.isArtinianRing_of_krullDimLE_zeroproof · cited by 2
- IsSemiprimaryRing.inductionproof · cited by 2
- isSemiprimaryRing_iffstatement and proof · cited by 1
- IsArtinianRing.isSemisimpleRing_of_isReducedstatement · cited by 1
- IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finitestatement and proof · cited by 1
- IsSemisimpleRing.exists_linearEquiv_ideal_of_isSimpleModulestatement and proof · cited by 1
- IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRingstatement and proof · cited by 1
- Module.finite_of_isSemisimpleRingstatement and proof · cited by 1