algebra.ring.prod - mathlib docs

source

@[protected, instance]

def prod.distrib {R : Type u_1} {S : Type u_3} [distrib R] [distrib S] :

distrib (R × S)

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 := _}

source

@[protected, instance]

def prod.non_unital_non_assoc_semiring {R : Type u_1} {S : Type u_3} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :

non_unital_non_assoc_semiring (R × S)

Product of two non_unital_non_assoc_semirings is a non_unital_non_assoc_semiring.

Equations

prod.non_unital_non_assoc_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 := mul_zero_class.mul prod.mul_zero_class, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.non_unital_semiring {R : Type u_1} {S : Type u_3} [non_unital_semiring R] [non_unital_semiring S] :

non_unital_semiring (R × S)

Product of two non_unital_semirings is a non_unital_semiring.

Equations

prod.non_unital_semiring = {add := non_unital_non_assoc_semiring.add prod.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero prod.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul prod.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

source

@[protected, instance]

def prod.non_assoc_semiring {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

non_assoc_semiring (R × S)

Product of two non_assoc_semirings is a non_assoc_semiring.

Equations

prod.non_assoc_semiring = {add := non_unital_non_assoc_semiring.add prod.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero prod.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul prod.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := mul_one_class.one prod.mul_one_class, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast prod.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _}

source

@[protected, instance]

def prod.semiring {R : Type u_1} {S : Type u_3} [semiring R] [semiring S] :

semiring (R × S)

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, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := monoid_with_zero.one prod.monoid_with_zero, one_mul := _, mul_one := _, nat_cast := add_monoid_with_one.nat_cast prod.add_monoid_with_one, nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow prod.monoid_with_zero, npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def prod.non_unital_comm_semiring {R : Type u_1} {S : Type u_3} [non_unital_comm_semiring R] [non_unital_comm_semiring S] :

non_unital_comm_semiring (R × S)

Product of two non_unital_comm_semirings is a non_unital_comm_semiring.

Equations

prod.non_unital_comm_semiring = {add := non_unital_semiring.add prod.non_unital_semiring, add_assoc := _, zero := non_unital_semiring.zero prod.non_unital_semiring, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul prod.non_unital_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul prod.non_unital_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

source

@[protected, 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, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one prod.semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast prod.semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def prod.non_unital_non_assoc_ring {R : Type u_1} {S : Type u_3} [non_unital_non_assoc_ring R] [non_unital_non_assoc_ring S] :

non_unital_non_assoc_ring (R × S)

Equations

prod.non_unital_non_assoc_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 := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul prod.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.non_unital_ring {R : Type u_1} {S : Type u_3} [non_unital_ring R] [non_unital_ring S] :

non_unital_ring (R × S)

Equations

prod.non_unital_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 := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_semiring.mul prod.non_unital_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

source

@[protected, instance]

def prod.non_assoc_ring {R : Type u_1} {S : Type u_3} [non_assoc_ring R] [non_assoc_ring S] :

non_assoc_ring (R × S)

Equations

prod.non_assoc_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 := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_assoc_semiring.mul prod.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := non_assoc_semiring.one prod.non_assoc_semiring, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast prod.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast prod.add_group_with_one, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[protected, instance]

def prod.ring {R : Type u_1} {S : Type u_3} [ring R] [ring S] :

ring (R × S)

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 := _, zsmul := add_comm_group.zsmul prod.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast prod.add_group_with_one, nat_cast := add_group_with_one.nat_cast prod.add_group_with_one, one := add_group_with_one.one prod.add_group_with_one, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul prod.semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow prod.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}

source

@[protected, instance]

def prod.non_unital_comm_ring {R : Type u_1} {S : Type u_3} [non_unital_comm_ring R] [non_unital_comm_ring S] :

non_unital_comm_ring (R × S)

Product of two non_unital_comm_rings is a non_unital_comm_ring.

Equations

prod.non_unital_comm_ring = {add := non_unital_ring.add prod.non_unital_ring, add_assoc := _, zero := non_unital_ring.zero prod.non_unital_ring, zero_add := _, add_zero := _, nsmul := non_unital_ring.nsmul prod.non_unital_ring, nsmul_zero' := _, nsmul_succ' := _, neg := non_unital_ring.neg prod.non_unital_ring, sub := non_unital_ring.sub prod.non_unital_ring, sub_eq_add_neg := _, zsmul := non_unital_ring.zsmul prod.non_unital_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_ring.mul prod.non_unital_ring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

source

@[protected, instance]

def prod.comm_ring {R : Type u_1} {S : Type u_3} [comm_ring R] [comm_ring S] :

comm_ring (R × S)

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 := _, zsmul := ring.zsmul prod.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast prod.ring, nat_cast := ring.nat_cast prod.ring, one := ring.one prod.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul prod.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow prod.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

def non_unital_ring_hom.fst (R : Type u_1) (S : Type u_3) [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :

R × S →ₙ+* R

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

Equations

non_unital_ring_hom.fst R S = {to_fun := prod.fst S, map_mul' := _, map_zero' := _, map_add' := _}

source

def non_unital_ring_hom.snd (R : Type u_1) (S : Type u_3) [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :

R × S →ₙ+* S

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

Equations

non_unital_ring_hom.snd R S = {to_fun := prod.snd S, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem non_unital_ring_hom.coe_fst {R : Type u_1} {S : Type u_3} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :

⇑(non_unital_ring_hom.fst R S) = prod.fst

source

@[simp]

theorem non_unital_ring_hom.coe_snd {R : Type u_1} {S : Type u_3} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] :

⇑(non_unital_ring_hom.snd R S) = prod.snd

source

@[protected]

def non_unital_ring_hom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring 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

f.prod g = {to_fun := λ (x : R), (⇑f x, ⇑g x), map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem non_unital_ring_hom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :

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

source

@[simp]

theorem non_unital_ring_hom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :

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

source

@[simp]

theorem non_unital_ring_hom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :

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

source

theorem non_unital_ring_hom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring T] (f : R →ₙ+* S × T) :

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

source

def non_unital_ring_hom.prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

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

prod.map as a non_unital_ring_hom.

Equations

f.prod_map g = (f.comp (non_unital_ring_hom.fst R S)).prod (g.comp (non_unital_ring_hom.snd R S))

source

theorem non_unital_ring_hom.prod_map_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

f.prod_map g = (f.comp (non_unital_ring_hom.fst R S)).prod (g.comp (non_unital_ring_hom.snd R S))

source

@[simp]

theorem non_unital_ring_hom.coe_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

theorem non_unital_ring_hom.prod_comp_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [non_unital_non_assoc_semiring R] [non_unital_non_assoc_semiring S] [non_unital_non_assoc_semiring R'] [non_unital_non_assoc_semiring S'] [non_unital_non_assoc_semiring T] (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def ring_hom.fst (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] :

R × S →+* R

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

Equations

ring_hom.fst R S = {to_fun := prod.fst S, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

def ring_hom.snd (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] :

R × S →+* S

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

Equations

ring_hom.snd R S = {to_fun := prod.snd S, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem ring_hom.coe_fst {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

⇑(ring_hom.fst R S) = prod.fst

source

@[simp]

theorem ring_hom.coe_snd {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

⇑(ring_hom.snd R S) = prod.snd

source

@[protected]

def ring_hom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring 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

f.prod g = {to_fun := λ (x : R), (⇑f x, ⇑g x), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem ring_hom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring T] (f : R →+* S) (g : R →+* T) (x : R) :

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

source

@[simp]

theorem ring_hom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring T] (f : R →+* S) (g : R →+* T) :

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

source

@[simp]

theorem ring_hom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring T] (f : R →+* S) (g : R →+* T) :

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

source

theorem ring_hom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring T] (f : R →+* S × T) :

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

source

def ring_hom.prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] (f : R →+* R') (g : S →+* S') :

R × S →+* R' × S'

prod.map as a ring_hom.

Equations

f.prod_map g = (f.comp (ring_hom.fst R S)).prod (g.comp (ring_hom.snd R S))

source

theorem ring_hom.prod_map_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] (f : R →+* R') (g : S →+* S') :

f.prod_map g = (f.comp (ring_hom.fst R S)).prod (g.comp (ring_hom.snd R S))

source

@[simp]

theorem ring_hom.coe_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] (f : R →+* R') (g : S →+* S') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

theorem ring_hom.prod_comp_prod_map {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [non_assoc_semiring R] [non_assoc_semiring S] [non_assoc_semiring R'] [non_assoc_semiring S'] [non_assoc_semiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def ring_equiv.prod_comm {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

R × S ≃+* S × R

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' := _}

source

@[simp]

theorem ring_equiv.coe_prod_comm {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

⇑ring_equiv.prod_comm = prod.swap

source

@[simp]

theorem ring_equiv.coe_prod_comm_symm {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

⇑(ring_equiv.prod_comm.symm) = prod.swap

source

@[simp]

theorem ring_equiv.fst_comp_coe_prod_comm {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

(ring_hom.fst S R).comp ↑ring_equiv.prod_comm = ring_hom.snd R S

source

@[simp]

theorem ring_equiv.snd_comp_coe_prod_comm {R : Type u_1} {S : Type u_3} [non_assoc_semiring R] [non_assoc_semiring S] :

(ring_hom.snd S R).comp ↑ring_equiv.prod_comm = ring_hom.fst R S

source

def ring_equiv.prod_zero_ring (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] :

R ≃+* R × S

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

Equations

ring_equiv.prod_zero_ring R S = {to_fun := λ (x : R), (x, 0), inv_fun := prod.fst S, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ring_equiv.prod_zero_ring_symm_apply (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (self : R × S) :

⇑((ring_equiv.prod_zero_ring R S).symm) self = self.fst

source

@[simp]

theorem ring_equiv.prod_zero_ring_apply (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (x : R) :

⇑(ring_equiv.prod_zero_ring R S) x = (x, 0)

source

def ring_equiv.zero_ring_prod (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] :

R ≃+* S × R

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

Equations

ring_equiv.zero_ring_prod R S = {to_fun := λ (x : R), (0, x), inv_fun := prod.snd R, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}

source

@[simp]

theorem ring_equiv.zero_ring_prod_apply (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (x : R) :

⇑(ring_equiv.zero_ring_prod R S) x = (0, x)

source

@[simp]

theorem ring_equiv.zero_ring_prod_symm_apply (R : Type u_1) (S : Type u_3) [non_assoc_semiring R] [non_assoc_semiring S] [subsingleton S] (self : S × R) :

⇑((ring_equiv.zero_ring_prod R S).symm) self = self.snd

source

theorem false_of_nontrivial_of_product_domain (R : Type u_1) (S : Type u_2) [ring R] [ring S] [is_domain (R × S)] [nontrivial R] [nontrivial S] :

false

The product of two nontrivial rings is not a domain

mathlib documentation

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

Semiring, ring etc structures on R × S #

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