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 ring_hom
s:
@[instance]
Product of two distributive types is distributive.
Equations
- prod.distrib = {mul := has_mul.mul prod.has_mul, add := has_add.add prod.has_add, left_distrib := _, right_distrib := _}
@[instance]
Product of two semirings is a semiring.
Equations
- prod.semiring = {add := add_comm_monoid.add prod.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero prod.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul prod.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid_with_zero.mul prod.monoid_with_zero, mul_assoc := _, one := monoid_with_zero.one prod.monoid_with_zero, one_mul := _, mul_one := _, npow := monoid_with_zero.npow prod.monoid_with_zero, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
@[instance]
def
prod.comm_semiring
{R : Type u_1}
{S : Type u_3}
[comm_semiring R]
[comm_semiring S] :
comm_semiring (R × S)
Product of two commutative semirings is a commutative semiring.
Equations
- prod.comm_semiring = {add := semiring.add prod.semiring, add_assoc := _, zero := semiring.zero prod.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul prod.semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul prod.semiring, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[instance]
Product of two rings is a ring.
Equations
- prod.ring = {add := add_comm_group.add prod.add_comm_group, add_assoc := _, zero := add_comm_group.zero prod.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul prod.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg prod.add_comm_group, sub := add_comm_group.sub prod.add_comm_group, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := semiring.mul prod.semiring, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[instance]
Product of two commutative rings is a commutative ring.
Equations
- prod.comm_ring = {add := ring.add prod.ring, add_assoc := _, zero := ring.zero prod.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul prod.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg prod.ring, sub := ring.sub prod.ring, sub_eq_add_neg := _, add_left_neg := _, add_comm := _, mul := ring.mul prod.ring, mul_assoc := _, one := ring.one prod.ring, one_mul := _, mul_one := _, npow := ring.npow prod.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[simp]
theorem
ring_hom.coe_fst
{R : Type u_1}
{S : Type u_3}
[semiring R]
[semiring S] :
⇑(ring_hom.fst R S) = prod.fst
@[simp]
theorem
ring_hom.coe_snd
{R : Type u_1}
{S : Type u_3}
[semiring R]
[semiring S] :
⇑(ring_hom.snd R S) = prod.snd
theorem
ring_hom.prod_unique
{R : Type u_1}
{S : Type u_3}
{T : Type u_5}
[semiring R]
[semiring S]
[semiring T]
(f : R →+* S × T) :
((ring_hom.fst S T).comp f).prod ((ring_hom.snd S T).comp f) = f
def
ring_hom.prod_map
{R : Type u_1}
{R' : Type u_2}
{S : Type u_3}
{S' : Type u_4}
[semiring R]
[semiring S]
[semiring R']
[semiring S']
(f : R →+* R')
(g : S →+* S') :
Equations
- f.prod_map g = ↑((f.comp (ring_hom.fst R S)).prod (g.comp (ring_hom.snd R S)))
Swapping components as an equivalence of (semi)rings.
Equations
- ring_equiv.prod_comm = {to_fun := add_equiv.prod_comm.to_fun, inv_fun := add_equiv.prod_comm.inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[simp]
@[simp]
@[simp]
theorem
ring_equiv.fst_comp_coe_prod_comm
{R : Type u_1}
{S : Type u_3}
[semiring R]
[semiring S] :
(ring_hom.fst S R).comp ↑ring_equiv.prod_comm = ring_hom.snd R S
@[simp]
theorem
ring_equiv.snd_comp_coe_prod_comm
{R : Type u_1}
{S : Type u_3}
[semiring R]
[semiring S] :
(ring_hom.snd S R).comp ↑ring_equiv.prod_comm = ring_hom.fst R S