Structures · Algebra
IsSimpleRing
A ring R is simple if it has only two two-sided ideals, namely ⊥ and ⊤.
- Defined in
- Mathlib.RingTheory.SimpleRing.Defs
- Shape
- One type argument · adds simple
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Matrix
- AlgCat.carrier
- MulOpposite
How is a type an instance?
Loading the hierarchy index…
Assumed by35
- RingHom.injective
- Polynomial.map_ne_zero
- Polynomial.natDegree_map
- Polynomial.leadingCoeff_map
- Polynomial.degree_map
- Polynomial.map_eq_zero
- IsSimpleRing.isIsotypic
- Polynomial.nextCoeff_map_eq
- IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite
- AlgHom.bijective
- IsSimpleRing.injective_ringHom_or_subsingleton_codomain
- IsSimpleRing.one_mem_of_ne_zero_mem
- IsSimpleRing.one_mem_of_ne_bot
- IsSimpleRing.tfae
- IsSimpleRing.isSemisimpleRing_iff_isArtinianRing
- IsSimpleRing.isField_center
- IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite
- IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite
- IsSimpleRing.exists_algEquiv_matrix_divisionRing
- IsSimpleRing.matrix
- Polynomial.monic_map_iff
- IsDomain.of_isSimpleRing
- instIsSimpleOrderIdeal
- IsPrincipalIdealRing.of_isSimpleRing
- IsSimpleRing.exists_algEquiv_matrix_of_isAlgClosed
- IsSimpleRing.instIsSemisimpleRing
- IsSimpleRing.simple
- IsSimpleRing.instNontrivial
- AbsoluteValue.LiesOver.congr_simp
- IsAlgClosed.exists_eval₂_eq_zero
- instFaithfulSMul_1
- IsSepClosed.exists_eval₂_eq_zero
- IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing
- IsSimpleRing.instMulOpposite
- IsSimpleRing.exists_ringEquiv_matrix_divisionRing
Ancestors0
No ancestors.