Theorems · Theorem · commutative algebra
Module.finite_of_isSemisimpleRing
∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.FiniteType R A] [IsJacobsonRing R] [IsSemisimpleRing A], Module.Finite R A
- Defined in
- Mathlib.RingTheory.Jacobson.Artinian
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- HasQuotient.Quotientproof · cited by 2,301
- LinearEquiv.symmproof · cited by 1,461
- Module.Finitestatement and proof · cited by 1,032
- AlgEquiv.toLinearEquivproof · cited by 117
- Algebra.FiniteTypestatement and proof · cited by 84
- MaximalSpectrumproof · cited by 73
- AlgEquiv.restrictScalarsproof · cited by 60
- MaximalSpectrum.asIdealproof · cited by 58
- IsJacobsonRingstatement and proof · cited by 40
- IsSemisimpleRingstatement and proof · cited by 28
Cited by1
Results whose statement or proof uses this declaration.
- Module.finite_of_isArtinianRingproof · cited by 1