Bundled non-unital subsemirings #
We define bundled non-unital subsemirings and some standard constructions:
subtype
and inclusion
ring homomorphisms.
NonUnitalSubsemiringClass S R
states that S
is a type of subsets s ⊆ R
that
are both an additive submonoid and also a multiplicative subsemigroup.
Instances
A non-unital subsemiring of a NonUnitalNonAssocSemiring
inherits a
NonUnitalNonAssocSemiring
structure
Equations
The natural non-unital ring hom from a non-unital subsemiring of a non-unital semiring R
to
R
.
Equations
Instances For
Alias of NonUnitalSubsemiringClass.coe_subtype
.
A non-unital subsemiring of a NonUnitalSemiring
is a NonUnitalSemiring
.
Equations
A non-unital subsemiring of a NonUnitalCommSemiring
is a NonUnitalCommSemiring
.
Equations
Note: currently, there are no ordered versions of non-unital rings.
A non-unital subsemiring of a non-unital semiring R
is a subset s
that is both an additive
submonoid and a semigroup.
Instances For
Equations
The actual NonUnitalSubsemiring
obtained from an element of a NonUnitalSubsemiringClass
.
Equations
Instances For
Two non-unital subsemirings are equal if they have the same elements.
Copy of a non-unital subsemiring with a new carrier
equal to the old one. Useful to fix
definitional equalities.
Equations
Instances For
Construct a NonUnitalSubsemiring R
from a set s
, a subsemigroup sg
, and an additive
submonoid sa
such that x ∈ s ↔ x ∈ sg ↔ x ∈ sa
.
Equations
Instances For
Note: currently, there are no ordered versions of non-unital rings.
The non-unital subsemiring R
of the non-unital semiring R
.
Equations
Equations
Equations
The inf of two non-unital subsemirings is their intersection.
Equations
Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.
Equations
Instances For
The non-unital subsemiring of elements x : R
such that f x = g x
Equations
Instances For
The non-unital ring homomorphism associated to an inclusion of non-unital subsemirings.