Theorems · Inductive type · ring theory
IsSimpleRing
(R : Type u_1) → [NonUnitalNonAssocRing R] → Prop
A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.
- Defined in
- Mathlib.RingTheory.SimpleRing.Defs
- Cited by
- 39 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- NonUnitalNonAssocRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- NonUnitalNonAssocRingstatement · cited by 354
Cited by49
Results whose statement or proof uses this declaration.
- RingHom.injectivestatement and proof · cited by 187
- Polynomial.map_ne_zerostatement and proof · cited by 22
- Polynomial.natDegree_mapstatement and proof · cited by 21
- Polynomial.leadingCoeff_mapstatement and proof · cited by 11
- Polynomial.degree_mapstatement and proof · cited by 10
- AbsoluteValue.LiesOver.comp_eqstatement and proof · cited by 4
- Polynomial.map_eq_zerostatement and proof · cited by 4
- AbsoluteValue.LiesOverstatement · cited by 2
- AlgHom.bijectivestatement and proof · cited by 2
- Polynomial.nextCoeff_map_eqstatement and proof · cited by 2
- IsSimpleRing.exists_algEquiv_matrix_end_mulOppositestatement and proof · cited by 2
- IsSimpleRing.injective_ringHom_or_subsingleton_codomainstatement and proof · cited by 2