Semiring, ring etc structures on R × S
#
In this file we define two-binop (Semiring
, Ring
etc) structures on R × S
. We also prove
trivial simp
lemmas, and define the following operations on RingHom
s and similarly for
NonUnitalRingHom
s:
Product of two NonUnitalNonAssocSemiring
s is a NonUnitalNonAssocSemiring
.
Product of two NonUnitalSemiring
s is a NonUnitalSemiring
.
Product of two NonAssocSemiring
s is a NonAssocSemiring
.
Product of two NonUnitalCommSemiring
s is a NonUnitalCommSemiring
.
Product of two commutative semirings is a commutative semiring.
Product of two NonUnitalCommRing
s is a NonUnitalCommRing
.
Given non-unital semirings R
, S
, the natural projection homomorphism from R × S
to R
.
Instances For
Given non-unital semirings R
, S
, the natural projection homomorphism from R × S
to S
.
Instances For
Combine two non-unital ring homomorphisms f : R →ₙ+* S
, g : R →ₙ+* T
into
f.prod g : R →ₙ+* S × T
given by (f.prod g) x = (f x, g x)
Instances For
Prod.map
as a NonUnitalRingHom
.
Instances For
Given semirings R
, S
, the natural projection homomorphism from R × S
to R
.
Instances For
Given semirings R
, S
, the natural projection homomorphism from R × S
to S
.
Instances For
Combine two ring homomorphisms f : R →+* S
, g : R →+* T
into f.prod g : R →+* S × T
given by (f.prod g) x = (f x, g x)
Instances For
Instances For
Swapping components as an equivalence of (semi)rings.
Instances For
Four-way commutativity of prod
. The name matches mul_mul_mul_comm
.
Instances For
A ring R
is isomorphic to R × S
when S
is the zero ring
Instances For
A ring R
is isomorphic to S × R
when S
is the zero ring
Instances For
The product of two nontrivial rings is not a domain