Bundled subsemirings #
We define bundled subsemirings and some standard constructions: subtype
and inclusion
ring homomorphisms.
AddSubmonoidWithOneClass S R
says S
is a type of subsets s ≤ R
that contain 0
, 1
,
and are closed under (+)
Instances
Equations
SubsemiringClass S R
states that S
is a type of subsets s ⊆ R
that
are both a multiplicative and an additive submonoid.
Instances
A subsemiring of a NonAssocSemiring
inherits a NonAssocSemiring
structure
Equations
The natural ring hom from a subsemiring of semiring R
to R
.
Equations
Instances For
A subsemiring of a Semiring
is a Semiring
.
Equations
A subsemiring of a CommSemiring
is a CommSemiring
.
Equations
A subsemiring of a semiring R
is a subset s
that is both a multiplicative and an additive
submonoid.
Instances For
Equations
The actual Subsemiring
obtained from an element of a SubsemiringClass
.
Equations
Instances For
Turn a Subsemiring
into a NonUnitalSubsemiring
by forgetting that it contains 1
.
Equations
Instances For
Two subsemirings are equal if they have the same elements.
Copy of a subsemiring with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
Instances For
Construct a Subsemiring R
from a set s
, a submonoid sm
, and an additive
submonoid sa
such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa
.
Equations
Instances For
A subsemiring contains the semiring's 1.
A subsemiring contains the semiring's 0.
A subsemiring is closed under multiplication.
A subsemiring is closed under addition.
A subsemiring of a NonAssocSemiring
inherits a NonAssocSemiring
structure
Equations
A subsemiring of a CommSemiring
is a CommSemiring
.
Equations
The natural ring hom from a subsemiring of semiring R
to R
.
Equations
Instances For
The subsemiring R
of the semiring R
.
Equations
The inf of two subsemirings is their intersection.
Equations
Restriction of a ring homomorphism to a subsemiring of the domain.
Equations
Instances For
The subsemiring of elements x : R
such that f x = g x
Equations
Instances For
Turn a non-unital subsemiring containing 1
into a subsemiring.