Structures · Algebra
NonUnitalSubsemiringClass
NonUnitalSubsemiringClass S R states that S is a type of subsets s ⊆ R that
are both an additive submonoid and also a multiplicative subsemigroup.
- Shape
- 2 explicit arguments · adds mul_mem
Extends1
Extended by1
Concrete types that are instances5
- NonUnitalSubalgebra
- NonUnitalStarSubalgebra
- NonUnitalSubsemiring
- NonUnitalStarSubsemiring
- Ideal
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- NonUnitalSubalgebraClass.subtype
- NonUnitalStarSubalgebraClass.subtype
- NonUnitalSubsemiringClass.subtype
- NonUnitalStarSubalgebra.unitization
- NonUnitalSubalgebra.unitization
- NonUnitalSubalgebra.unitization_range
- NonUnitalSubsemiring.unitization
- NonUnitalStarSubalgebra.ofClass
- NonUnitalSubalgebra.ofClass
- NonUnitalSubsemiring.ofClass
- NonUnitalStarSubalgebra.ofClass_carrier
- NonUnitalStarSubsemiring.ofClass
- NonUnitalSubsemiring.unitization_range
- NonUnitalStarSubalgebraClass.coe_subtype
- NonUnitalSubsemiringClass.toNonUnitalCommSemiring
- NonUnitalSubsemiringClass.toAddSubmonoidClass
- NonUnitalSubsemiringClass.toNonUnitalNonAssocCommSemiring
- NonUnitalSubalgebraClass.coe_subtype
- NonUnitalSubsemiringClass.mul_mem
- NonUnitalSubsemiringClass.coe_subtype
- NonUnitalSubsemiring.unitization_apply
- NonUnitalSubalgebraClass.subtype_apply
- NonUnitalSubsemiringClass.mulMemClass
- NonUnitalSubsemiringClass.subtype_apply
- NonUnitalSubsemiringClass.subtype_injective
- NonUnitalStarSubalgebra.unitization.congr_simp
- NonUnitalSubsemiringClass.toNonUnitalNonAssocSemiring
- NonUnitalStarSubsemiring.coe_ofClass
- NonUnitalSubsemiringClass.toNonUnitalSemiring
- NonUnitalStarSubalgebraClass.subtype_apply
- NonUnitalStarSubalgebra.unitization_apply
- NonUnitalSubsemiring.ofClass_carrier
- StarMemClass.instStarRing
- NonUnitalSubalgebra.unitization_apply
- NonUnitalStarSubalgebra.ofClass.congr_simp
- NonUnitalStarSubalgebraClass.subtype_injective
- NonUnitalRingHom.codRestrict
- NonUnitalSubalgebra.ofClass_carrier
- NonUnitalSubalgebraClass.subtype_injective
- NonUnitalStarSubalgebra.unitization_range
- NonUnitalSubsemiringClass.noZeroDivisors