# 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 RingHoms and similarly for NonUnitalRingHoms:

• fst R S : R × S →+* R, snd R S : R × S →+* S: projections Prod.fst and Prod.snd as RingHoms;
• f.prod g : R →+* S × T: sends x to (f x, g x);
• f.prod_map g : R × S → R' × S': Prod.map f g as a RingHom, sends (x, y) to (f x, g y).
instance Prod.instDistrib {R : Type u_3} {S : Type u_5} [] [] :
Distrib (R × S)

Product of two distributive types is distributive.

Equations
• Prod.instDistrib =
instance Prod.instNonUnitalNonAssocSemiring {R : Type u_3} {S : Type u_5} :

Product of two NonUnitalNonAssocSemirings is a NonUnitalNonAssocSemiring.

Equations
• One or more equations did not get rendered due to their size.
instance Prod.instNonUnitalSemiring {R : Type u_3} {S : Type u_5} :

Product of two NonUnitalSemirings is a NonUnitalSemiring.

Equations
instance Prod.instNonAssocSemiring {R : Type u_3} {S : Type u_5} [] [] :

Product of two NonAssocSemirings is a NonAssocSemiring.

Equations
• One or more equations did not get rendered due to their size.
instance Prod.instSemiring {R : Type u_3} {S : Type u_5} [] [] :
Semiring (R × S)

Product of two semirings is a semiring.

Equations
• One or more equations did not get rendered due to their size.

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

Equations
instance Prod.instCommSemiring {R : Type u_3} {S : Type u_5} [] [] :

Product of two commutative semirings is a commutative semiring.

Equations
Equations
instance Prod.instNonUnitalRing {R : Type u_3} {S : Type u_5} [] [] :
Equations
instance Prod.instNonAssocRing {R : Type u_3} {S : Type u_5} [] [] :
Equations
• One or more equations did not get rendered due to their size.
instance Prod.instRing {R : Type u_3} {S : Type u_5} [Ring R] [Ring S] :
Ring (R × S)

Product of two rings is a ring.

Equations
• One or more equations did not get rendered due to their size.
instance Prod.instNonUnitalCommRing {R : Type u_3} {S : Type u_5} :

Product of two NonUnitalCommRings is a NonUnitalCommRing.

Equations
instance Prod.instCommRing {R : Type u_3} {S : Type u_5} [] [] :
CommRing (R × S)

Product of two commutative rings is a commutative ring.

Equations
def NonUnitalRingHom.fst (R : Type u_3) (S : Type u_5) :
R × S →ₙ+* R

Given non-unital semirings R, S, the natural projection homomorphism from R × S to R.

Equations
• = let __src := ; let __src := ; { toFun := Prod.fst, map_mul' := , map_zero' := , map_add' := }
Instances For
def NonUnitalRingHom.snd (R : Type u_3) (S : Type u_5) :
R × S →ₙ+* S

Given non-unital semirings R, S, the natural projection homomorphism from R × S to S.

Equations
• = let __src := ; let __src := ; { toFun := Prod.snd, map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem NonUnitalRingHom.coe_fst {R : Type u_3} {S : Type u_5} :
() = Prod.fst
@[simp]
theorem NonUnitalRingHom.coe_snd {R : Type u_3} {S : Type u_5} :
() = Prod.snd
def NonUnitalRingHom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} (f : R →ₙ+* S) (g : R →ₙ+* T) :
R →ₙ+* S × T

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)

Equations
• f.prod g = let __src := (f).prod g; let __src := (f).prod g; { toFun := fun (x : R) => (f x, g x), map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem NonUnitalRingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :
(f.prod g) x = (f x, g x)
@[simp]
theorem NonUnitalRingHom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} (f : R →ₙ+* S) (g : R →ₙ+* T) :
().comp (f.prod g) = f
@[simp]
theorem NonUnitalRingHom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} (f : R →ₙ+* S) (g : R →ₙ+* T) :
().comp (f.prod g) = g
theorem NonUnitalRingHom.prod_unique {R : Type u_3} {S : Type u_5} {T : Type u_7} (f : R →ₙ+* S × T) :
(().comp f).prod (().comp f) = f
def NonUnitalRingHom.prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} (f : R →ₙ+* R') (g : S →ₙ+* S') :
R × S →ₙ+* R' × S'

Prod.map as a NonUnitalRingHom.

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
theorem NonUnitalRingHom.prodMap_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} (f : R →ₙ+* R') (g : S →ₙ+* S') :
f.prodMap g = (f.comp ()).prod (g.comp ())
@[simp]
theorem NonUnitalRingHom.coe_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} (f : R →ₙ+* R') (g : S →ₙ+* S') :
(f.prodMap g) = Prod.map f g
theorem NonUnitalRingHom.prod_comp_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} {T : Type u_7} (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def RingHom.fst (R : Type u_3) (S : Type u_5) [] [] :
R × S →+* R

Given semirings R, S, the natural projection homomorphism from R × S to R.

Equations
• = let __src := ; let __src := ; { toFun := Prod.fst, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
def RingHom.snd (R : Type u_3) (S : Type u_5) [] [] :
R × S →+* S

Given semirings R, S, the natural projection homomorphism from R × S to S.

Equations
• = let __src := ; let __src := ; { toFun := Prod.snd, map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
instance RingHom.instRingHomSurjectiveProdFst (R : Type u_9) (S : Type u_10) [] [] :
Equations
• =
instance RingHom.instRingHomSurjectiveProdSnd (R : Type u_9) (S : Type u_10) [] [] :
Equations
• =
@[simp]
theorem RingHom.coe_fst {R : Type u_3} {S : Type u_5} [] [] :
() = Prod.fst
@[simp]
theorem RingHom.coe_snd {R : Type u_3} {S : Type u_5} [] [] :
() = Prod.snd
def RingHom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [] [] [] (f : R →+* S) (g : R →+* T) :
R →+* S × T

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)

Equations
• f.prod g = let __src := (f).prod g; let __src := (f).prod g; { toFun := fun (x : R) => (f x, g x), map_one' := , map_mul' := , map_zero' := , map_add' := }
Instances For
@[simp]
theorem RingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [] [] [] (f : R →+* S) (g : R →+* T) (x : R) :
(f.prod g) x = (f x, g x)
@[simp]
theorem RingHom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [] [] [] (f : R →+* S) (g : R →+* T) :
().comp (f.prod g) = f
@[simp]
theorem RingHom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [] [] [] (f : R →+* S) (g : R →+* T) :
().comp (f.prod g) = g
theorem RingHom.prod_unique {R : Type u_3} {S : Type u_5} {T : Type u_7} [] [] [] (f : R →+* S × T) :
(().comp f).prod (().comp f) = f
def RingHom.prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [] [] [] [] (f : R →+* R') (g : S →+* S') :
R × S →+* R' × S'

Prod.map as a RingHom.

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
theorem RingHom.prodMap_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [] [] [] [] (f : R →+* R') (g : S →+* S') :
f.prodMap g = (f.comp ()).prod (g.comp ())
@[simp]
theorem RingHom.coe_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [] [] [] [] (f : R →+* R') (g : S →+* S') :
(f.prodMap g) = Prod.map f g
theorem RingHom.prod_comp_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} {T : Type u_7} [] [] [] [] [] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def RingEquiv.prodComm {R : Type u_3} {S : Type u_5} [] [] :
R × S ≃+* S × R

Swapping components as an equivalence of (semi)rings.

Equations
• RingEquiv.prodComm = let __src := AddEquiv.prodComm; let __src_1 := MulEquiv.prodComm; { toEquiv := __src.toEquiv, map_mul' := , map_add' := }
Instances For
@[simp]
theorem RingEquiv.coe_prodComm {R : Type u_3} {S : Type u_5} [] [] :
RingEquiv.prodComm = Prod.swap
@[simp]
theorem RingEquiv.coe_prodComm_symm {R : Type u_3} {S : Type u_5} [] [] :
RingEquiv.prodComm.symm = Prod.swap
@[simp]
theorem RingEquiv.fst_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [] [] :
().comp RingEquiv.prodComm =
@[simp]
theorem RingEquiv.snd_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [] [] :
().comp RingEquiv.prodComm =
@[simp]
theorem RingEquiv.prodProdProdComm_apply (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] (rrss : (R × R') × S × S') :
def RingEquiv.prodProdProdComm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] :
(R × R') × S × S' ≃+* (R × S) × R' × S'

Four-way commutativity of Prod. The name matches mul_mul_mul_comm.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem RingEquiv.prodProdProdComm_symm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] :
().symm =
@[simp]
theorem RingEquiv.prodProdProdComm_toAddEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] :
() =
@[simp]
theorem RingEquiv.prodProdProdComm_toMulEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] :
() =
@[simp]
theorem RingEquiv.prodProdProdComm_toEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [] [] [] [] :
() = Equiv.prodProdProdComm R R' S S'
@[simp]
theorem RingEquiv.prodZeroRing_apply (R : Type u_3) (S : Type u_5) [] [] [] (x : R) :
() x = (x, 0)
@[simp]
theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_3) (S : Type u_5) [] [] [] (self : R × S) :
().symm self = self.1
def RingEquiv.prodZeroRing (R : Type u_3) (S : Type u_5) [] [] [] :
R ≃+* R × S

A ring R is isomorphic to R × S when S is the zero ring

Equations
• = { toFun := fun (x : R) => (x, 0), invFun := Prod.fst, left_inv := , right_inv := , map_mul' := , map_add' := }
Instances For
@[simp]
theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_3) (S : Type u_5) [] [] [] (self : S × R) :
().symm self = self.2
@[simp]
theorem RingEquiv.zeroRingProd_apply (R : Type u_3) (S : Type u_5) [] [] [] (x : R) :
() x = (0, x)
def RingEquiv.zeroRingProd (R : Type u_3) (S : Type u_5) [] [] [] :
R ≃+* S × R

A ring R is isomorphic to S × R when S is the zero ring

Equations
• = { toFun := fun (x : R) => (0, x), invFun := Prod.snd, left_inv := , right_inv := , map_mul' := , map_add' := }
Instances For
theorem false_of_nontrivial_of_product_domain (R : Type u_9) (S : Type u_10) [Ring R] [Ring S] [IsDomain (R × S)] [] [] :

The product of two nontrivial rings is not a domain

### Order #

instance instOrderedSemiringProd {α : Type u_1} {β : Type u_2} [] [] :
Equations
instance instOrderedCommSemiringProd {α : Type u_1} {β : Type u_2} :
Equations
instance instOrderedRingProd {α : Type u_1} {β : Type u_2} [] [] :
OrderedRing (α × β)
Equations
instance instOrderedCommRingProd {α : Type u_1} {β : Type u_2} [] [] :
Equations