Structures · Algebra
NonUnitalSubringClass
NonUnitalSubringClass 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.RingTheory.NonUnitalSubring.Defs
- Shape
- 2 explicit arguments
Extends2
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- NonUnitalSubalgebra
- NonUnitalStarSubalgebra
- TwoSidedIdeal
- NonUnitalSubring
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by29
- NonUnitalSubringClass.subtype
- AlgHomClass.unitization_injective
- NonUnitalSubring.unitization
- NonUnitalStarSubalgebra.unitizationStarAlgEquiv
- AlgHomClass.unitization_injective'
- NonUnitalSubring.ofClass
- NonUnitalSubalgebra.unitizationAlgEquiv
- NonUnitalSubringClass.toNonUnitalCommRing
- NonUnitalSubringClass.toNonUnitalSubsemiringClass
- NonUnitalSubringClass.toNonUnitalNonAssocRing
- NonUnitalSubring.unitization_apply
- NonUnitalStarSubalgebra.unitization_injective
- cfcₙ_mem
- NonUnitalSubringClass.subtype_apply
- NonUnitalSubringClass.toNonUnitalNonAssocCommRing
- NonUnitalStarSubalgebra.nonUnitalCStarAlgebra
- NonUnitalStarSubalgebra.nonUnitalCommCStarAlgebra
- NonUnitalSubringClass.toNonUnitalRing
- NonUnitalSubring.ofClass_carrier
- NonUnitalSubringClass.addSubgroupClass
- NonUnitalSubringClass.subtype_injective
- NonUnitalSubalgebraClass.nonUnitalNormedRing
- NonUnitalSubalgebra.unitization_injective
- NonUnitalSubalgebraClass.nonUnitalSeminormedRing
- NonUnitalSubringClass.toNegMemClass
- NonUnitalSubringClass.coe_subtype
- NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe
- NonUnitalSubring.unitization_range
- NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe