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).

source

instance Prod.instDistrib {R : Type u_3} {S : Type u_5} [Distrib R] [Distrib S] :

Distrib (R × S)

Product of two distributive types is distributive.

Equations

Prod.instDistrib = Distrib.mk ⋯ ⋯

source

instance Prod.instNonUnitalNonAssocSemiring {R : Type u_3} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :

NonUnitalNonAssocSemiring (R × S)

Product of two NonUnitalNonAssocSemirings is a NonUnitalNonAssocSemiring.

Equations

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

source

instance Prod.instNonUnitalSemiring {R : Type u_3} {S : Type u_5} [NonUnitalSemiring R] [NonUnitalSemiring S] :

NonUnitalSemiring (R × S)

Product of two NonUnitalSemirings is a NonUnitalSemiring.

Equations

Prod.instNonUnitalSemiring = let __src := inferInstanceAs (NonUnitalNonAssocSemiring (R × S)); let __src_1 := inferInstanceAs (SemigroupWithZero (R × S)); NonUnitalSemiring.mk ⋯

source

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

NonAssocSemiring (R × S)

Product of two NonAssocSemirings is a NonAssocSemiring.

Equations

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

source

instance Prod.instSemiring {R : Type u_3} {S : Type u_5} [Semiring R] [Semiring S] :

Semiring (R × S)

Product of two semirings is a semiring.

Equations

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

source

instance Prod.instNonUnitalCommSemiring {R : Type u_3} {S : Type u_5} [NonUnitalCommSemiring R] [NonUnitalCommSemiring S] :

NonUnitalCommSemiring (R × S)

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

Equations

Prod.instNonUnitalCommSemiring = let __src := inferInstanceAs (NonUnitalSemiring (R × S)); let __src_1 := inferInstanceAs (CommSemigroup (R × S)); NonUnitalCommSemiring.mk ⋯

source

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

CommSemiring (R × S)

Product of two commutative semirings is a commutative semiring.

Equations

Prod.instCommSemiring = let __src := inferInstanceAs (Semiring (R × S)); let __src_1 := inferInstanceAs (CommMonoid (R × S)); CommSemiring.mk ⋯

source

instance Prod.instNonUnitalNonAssocRing {R : Type u_3} {S : Type u_5} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] :

NonUnitalNonAssocRing (R × S)

Equations

Prod.instNonUnitalNonAssocRing = let __src := inferInstanceAs (AddCommGroup (R × S)); let __src_1 := inferInstanceAs (NonUnitalNonAssocSemiring (R × S)); NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯

source

instance Prod.instNonUnitalRing {R : Type u_3} {S : Type u_5} [NonUnitalRing R] [NonUnitalRing S] :

NonUnitalRing (R × S)

Equations

Prod.instNonUnitalRing = let __src := inferInstanceAs (NonUnitalNonAssocRing (R × S)); let __src_1 := inferInstanceAs (NonUnitalSemiring (R × S)); NonUnitalRing.mk ⋯

source

instance Prod.instNonAssocRing {R : Type u_3} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] :

NonAssocRing (R × S)

Equations

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

source

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.

source

instance Prod.instNonUnitalCommRing {R : Type u_3} {S : Type u_5} [NonUnitalCommRing R] [NonUnitalCommRing S] :

NonUnitalCommRing (R × S)

Product of two NonUnitalCommRings is a NonUnitalCommRing.

Equations

Prod.instNonUnitalCommRing = let __src := inferInstanceAs (NonUnitalRing (R × S)); let __src_1 := inferInstanceAs (CommSemigroup (R × S)); NonUnitalCommRing.mk ⋯

source

instance Prod.instCommRing {R : Type u_3} {S : Type u_5} [CommRing R] [CommRing S] :

CommRing (R × S)

Product of two commutative rings is a commutative ring.

Equations

Prod.instCommRing = let __src := inferInstanceAs (Ring (R × S)); let __src_1 := inferInstanceAs (CommMonoid (R × S)); CommRing.mk ⋯

source

def NonUnitalRingHom.fst (R : Type u_3) (S : Type u_5) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :

R × S →ₙ+* R

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

Equations

NonUnitalRingHom.fst R S = let __src := MulHom.fst R S; let __src := AddMonoidHom.fst R S; { toMulHom := { toFun := Prod.fst, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

def NonUnitalRingHom.snd (R : Type u_3) (S : Type u_5) [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :

R × S →ₙ+* S

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

Equations

NonUnitalRingHom.snd R S = let __src := MulHom.snd R S; let __src := AddMonoidHom.snd R S; { toMulHom := { toFun := Prod.snd, map_mul' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem NonUnitalRingHom.coe_fst {R : Type u_3} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :

⇑(NonUnitalRingHom.fst R S) = Prod.fst

source

@[simp]

theorem NonUnitalRingHom.coe_snd {R : Type u_3} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :

⇑(NonUnitalRingHom.snd R S) = Prod.snd

source

def NonUnitalRingHom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (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

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

Instances For

source

@[simp]

theorem NonUnitalRingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :

(NonUnitalRingHom.prod f g) x = (f x, g x)

source

@[simp]

theorem NonUnitalRingHom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :

NonUnitalRingHom.comp (NonUnitalRingHom.fst S T) (NonUnitalRingHom.prod f g) = f

source

@[simp]

theorem NonUnitalRingHom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :

NonUnitalRingHom.comp (NonUnitalRingHom.snd S T) (NonUnitalRingHom.prod f g) = g

source

theorem NonUnitalRingHom.prod_unique {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S × T) :

NonUnitalRingHom.prod (NonUnitalRingHom.comp (NonUnitalRingHom.fst S T) f) (NonUnitalRingHom.comp (NonUnitalRingHom.snd S T) f) = f

source

def NonUnitalRingHom.prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

R × S →ₙ+* R' × S'

Prod.map as a NonUnitalRingHom.

Equations

NonUnitalRingHom.prodMap f g = NonUnitalRingHom.prod (NonUnitalRingHom.comp f (NonUnitalRingHom.fst R S)) (NonUnitalRingHom.comp g (NonUnitalRingHom.snd R S))

Instances For

source

theorem NonUnitalRingHom.prodMap_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

NonUnitalRingHom.prodMap f g = NonUnitalRingHom.prod (NonUnitalRingHom.comp f (NonUnitalRingHom.fst R S)) (NonUnitalRingHom.comp g (NonUnitalRingHom.snd R S))

source

@[simp]

theorem NonUnitalRingHom.coe_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

⇑(NonUnitalRingHom.prodMap f g) = Prod.map ⇑f ⇑g

source

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} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnitalNonAssocSemiring T] (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :

NonUnitalRingHom.comp (NonUnitalRingHom.prodMap f' g') (NonUnitalRingHom.prod f g) = NonUnitalRingHom.prod (NonUnitalRingHom.comp f' f) (NonUnitalRingHom.comp g' g)

source

def RingHom.fst (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] :

R × S →+* R

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

Equations

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

Instances For

source

def RingHom.snd (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] :

R × S →+* S

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

Equations

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

Instances For

source

instance RingHom.instRingHomSurjectiveProdInstSemiringFstToNonAssocSemiringToNonAssocSemiring (R : Type u_9) (S : Type u_10) [Semiring R] [Semiring S] :

RingHomSurjective (RingHom.fst R S)

Equations

⋯ = ⋯

source

instance RingHom.instRingHomSurjectiveProdInstSemiringSndToNonAssocSemiringToNonAssocSemiring (R : Type u_9) (S : Type u_10) [Semiring R] [Semiring S] :

RingHomSurjective (RingHom.snd R S)

Equations

⋯ = ⋯

source

@[simp]

theorem RingHom.coe_fst {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

⇑(RingHom.fst R S) = Prod.fst

source

@[simp]

theorem RingHom.coe_snd {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

⇑(RingHom.snd R S) = Prod.snd

source

def RingHom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (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

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

Instances For

source

@[simp]

theorem RingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R) :

(RingHom.prod f g) x = (f x, g x)

source

@[simp]

theorem RingHom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :

RingHom.comp (RingHom.fst S T) (RingHom.prod f g) = f

source

@[simp]

theorem RingHom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :

RingHom.comp (RingHom.snd S T) (RingHom.prod f g) = g

source

theorem RingHom.prod_unique {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S × T) :

RingHom.prod (RingHom.comp (RingHom.fst S T) f) (RingHom.comp (RingHom.snd S T) f) = f

source

def RingHom.prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :

R × S →+* R' × S'

Prod.map as a RingHom.

Equations

RingHom.prodMap f g = RingHom.prod (RingHom.comp f (RingHom.fst R S)) (RingHom.comp g (RingHom.snd R S))

Instances For

source

theorem RingHom.prodMap_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :

RingHom.prodMap f g = RingHom.prod (RingHom.comp f (RingHom.fst R S)) (RingHom.comp g (RingHom.snd R S))

source

@[simp]

theorem RingHom.coe_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :

⇑(RingHom.prodMap f g) = Prod.map ⇑f ⇑g

source

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} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] [NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :

RingHom.comp (RingHom.prodMap f' g') (RingHom.prod f g) = RingHom.prod (RingHom.comp f' f) (RingHom.comp g' g)

source

def RingEquiv.prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

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

source

@[simp]

theorem RingEquiv.coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

⇑RingEquiv.prodComm = Prod.swap

source

@[simp]

theorem RingEquiv.coe_prodComm_symm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

⇑(RingEquiv.symm RingEquiv.prodComm) = Prod.swap

source

@[simp]

theorem RingEquiv.fst_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

RingHom.comp (RingHom.fst S R) ↑RingEquiv.prodComm = RingHom.snd R S

source

@[simp]

theorem RingEquiv.snd_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :

RingHom.comp (RingHom.snd S R) ↑RingEquiv.prodComm = RingHom.fst R S

source

@[simp]

theorem RingEquiv.prodProdProdComm_apply (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (rrss : (R × R') × S × S') :

(RingEquiv.prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)

source

def RingEquiv.prodProdProdComm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :

(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

source

@[simp]

theorem RingEquiv.prodProdProdComm_symm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :

RingEquiv.symm (RingEquiv.prodProdProdComm R R' S S') = RingEquiv.prodProdProdComm R S R' S'

source

@[simp]

theorem RingEquiv.prodProdProdComm_toAddEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :

↑(RingEquiv.prodProdProdComm R R' S S') = AddEquiv.prodProdProdComm R R' S S'

source

@[simp]

theorem RingEquiv.prodProdProdComm_toMulEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :

↑(RingEquiv.prodProdProdComm R R' S S') = MulEquiv.prodProdProdComm R R' S S'

source

@[simp]

theorem RingEquiv.prodProdProdComm_toEquiv (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :

↑(RingEquiv.prodProdProdComm R R' S S') = Equiv.prodProdProdComm R R' S S'

source

@[simp]

theorem RingEquiv.prodZeroRing_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :

(RingEquiv.prodZeroRing R S) x = (x, 0)

source

@[simp]

theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : R × S) :

(RingEquiv.symm (RingEquiv.prodZeroRing R S)) self = self.1

source

def RingEquiv.prodZeroRing (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] :

R ≃+* R × S

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

Equations

RingEquiv.prodZeroRing R S = { toEquiv := { toFun := fun (x : R) => (x, 0), invFun := Prod.fst, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : S × R) :

(RingEquiv.symm (RingEquiv.zeroRingProd R S)) self = self.2

source

@[simp]

theorem RingEquiv.zeroRingProd_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :

(RingEquiv.zeroRingProd R S) x = (0, x)

source

def RingEquiv.zeroRingProd (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] :

R ≃+* S × R

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

Equations

RingEquiv.zeroRingProd R S = { toEquiv := { toFun := fun (x : R) => (0, x), invFun := Prod.snd, left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source

theorem false_of_nontrivial_of_product_domain (R : Type u_9) (S : Type u_10) [Ring R] [Ring S] [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] :

False

The product of two nontrivial rings is not a domain

Order #

source

instance instOrderedSemiringProd {α : Type u_1} {β : Type u_2} [OrderedSemiring α] [OrderedSemiring β] :

OrderedSemiring (α × β)

Equations

instOrderedSemiringProd = let __src := inferInstanceAs (Semiring (α × β)); let __src_1 := inferInstanceAs (OrderedAddCommMonoid (α × β)); OrderedSemiring.mk ⋯ ⋯ ⋯ ⋯

source

instance instOrderedCommSemiringProd {α : Type u_1} {β : Type u_2} [OrderedCommSemiring α] [OrderedCommSemiring β] :

OrderedCommSemiring (α × β)

Equations

instOrderedCommSemiringProd = let __src := inferInstanceAs (OrderedSemiring (α × β)); let __src_1 := inferInstanceAs (CommSemiring (α × β)); OrderedCommSemiring.mk ⋯

source

instance instOrderedRingProd {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedRing β] :

OrderedRing (α × β)

Equations

instOrderedRingProd = let __src := inferInstanceAs (Ring (α × β)); let __src_1 := inferInstanceAs (OrderedAddCommGroup (α × β)); OrderedRing.mk ⋯ ⋯ ⋯

source

instance instOrderedCommRingProd {α : Type u_1} {β : Type u_2} [OrderedCommRing α] [OrderedCommRing β] :

OrderedCommRing (α × β)

Equations

instOrderedCommRingProd = let __src := inferInstanceAs (OrderedRing (α × β)); let __src_1 := inferInstanceAs (CommRing (α × β)); OrderedCommRing.mk ⋯

Documentation

Mathlib.Algebra.Ring.Prod

Semiring, ring etc structures on `R × S` #

Order #

Semiring, ring etc structures on R × S #

Order #

Semiring, ring etc structures on `R × S` #