Structures · Algebra
SubringClass
SubringClass S R states that S is a type of subsets s ⊆ R that
are both a multiplicative submonoid and an additive subgroup.
- Defined in
- Mathlib.Algebra.Ring.Subring.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by1
Concrete types that are instances5
- StarSubalgebra
- ValuationSubring
- VonNeumannAlgebra
- Subalgebra
- Subring
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- intCast_mem
- SubringClass.subtype
- Subring.isIntegrallyClosedIn_iff
- Subring.ofClass
- Subalgebra.spectrum_sUnion_connectedComponentIn
- spectrum.subset_subalgebra
- Subalgebra.frontier_spectrum
- Subalgebra.isUnit_of_isUnit_val_of_eventually
- Subring.integralClosure_subring_le_iff
- RestrictedProduct.evalRingHom
- Subalgebra.spectrum_isBounded_connectedComponentIn
- Subalgebra.frontier_subset_frontier
- Subalgebra.spectrum_eq_of_isPreconnected_compl
- RestrictedProduct.mapAlongRingHom
- SubringClass.toNormMulClass
- RestrictedProduct.evalRingHom_apply
- Subring.toIsStrictOrderedRing
- SubringClass.coe_natCast
- Subring.isIntegrallyClosed_iff
- SubringClass.subtype_injective
- SubringClass.toNormOneClass
- RestrictedProduct.instIsTopologicalRingCoePrincipal
- SubringClass.toRing
- SubalgebraClass.normedRing
- RestrictedProduct.mapAlongRingHom_apply
- SubringClass.coe_subtype
- SubringClass.toSubsemiringClass
- SubringClass.toNormedCommRing
- Subring.toIsOrderedRing
- SubringClass.toSeminormedCommRing
- SubringClass.instIsDomainSubtypeMem
- SubringClass.toCommRing
- SubringClass.coe_intCast
- SubringClass.subtype_apply
- SubringClass.nonUnitalSubringClass
- StarSubalgebra.commCStarAlgebra
- RestrictedProduct.instRingCoeOfSubringClass
- RestrictedProduct.instIntCastCoeOfSubringClass
- SubringClass.toNonAssocRing
- cfc_mem
- Subring.coe_ofClass
- SubringClass.toSeminormedRing
- SubringClass.toHasIntCast
- SubalgebraClass.toNormedAlgebra
- RestrictedProduct.instCommRingCoeOfSubringClass
- SubringClass.toNonAssocCommRing
- SubalgebraClass.seminormedRing
- RestrictedProduct.isTopologicalRing
- SubringClass.toNegMemClass
- SubringClass.addSubgroupClass