IsSimpleRing

📁 Source: Mathlib/Algebra/Algebra/IsSimpleRing.lean

Statistics

Metric	Count
Definitions IsSimpleRing	1
Theorems instFaithfulSMul_1	1
Total	2

(root)

Definitions

Name	Category	Theorems
IsSimpleRing 📖	CompData	13 math math: IsSimpleRing.instMulOpposite, CSA.isSimple, IsSimpleRing.of_eq_bot_or_eq_top, isSimpleRing_iff, IsSimpleRing.matrix, isSimpleRing_iff_isTwoSided_imp, IsSimpleRing.of_surjective, DivisionRing.isSimpleRing, isSimpleRing_iff_isField, isSimpleRing_isArtinianRing_iff, IsSimpleRing.iff_injective_ringHom, IsSimpleRing.iff_injective_ringHom_or_subsingleton_codomain, IsSimpleRing.of_ringEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulSMul_1 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring	—	faithfulSMul_iff_algebraMap_injective RingHom.injective

---

← Back to Index