mathlib3 documentation

algebra.group.prod

Monoid, group etc structures on M × N #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define one-binop (monoid, group etc) structures on M × N. We also prove trivial simp lemmas, and define the following operations on monoid_homs:

Main declarations #

@[protected, instance]
def prod.has_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :
has_mul (M × N)
Equations
@[protected, instance]
def prod.has_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :
has_add (M × N)
Equations
@[simp]
theorem prod.fst_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
(p * q).fst = p.fst * q.fst
@[simp]
theorem prod.fst_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
(p + q).fst = p.fst + q.fst
@[simp]
theorem prod.snd_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
(p + q).snd = p.snd + q.snd
@[simp]
theorem prod.snd_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
(p * q).snd = p.snd * q.snd
@[simp]
theorem prod.mk_add_mk {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
@[simp]
theorem prod.mk_mul_mk {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
@[simp]
theorem prod.swap_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
(p * q).swap = p.swap * q.swap
@[simp]
theorem prod.swap_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
(p + q).swap = p.swap + q.swap
theorem prod.mul_def {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :
p * q = (p.fst * q.fst, p.snd * q.snd)
theorem prod.add_def {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :
p + q = (p.fst + q.fst, p.snd + q.snd)
theorem prod.zero_mk_add_zero_mk {M : Type u_5} {N : Type u_6} [add_monoid M] [has_add N] (b₁ b₂ : N) :
(0, b₁) + (0, b₂) = (0, b₁ + b₂)
theorem prod.one_mk_mul_one_mk {M : Type u_5} {N : Type u_6} [monoid M] [has_mul N] (b₁ b₂ : N) :
(1, b₁) * (1, b₂) = (1, b₁ * b₂)
theorem prod.mk_zero_add_mk_zero {M : Type u_5} {N : Type u_6} [has_add M] [add_monoid N] (a₁ a₂ : M) :
(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
theorem prod.mk_one_mul_mk_one {M : Type u_5} {N : Type u_6} [has_mul M] [monoid N] (a₁ a₂ : M) :
(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
@[protected, instance]
def prod.has_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
has_one (M × N)
Equations
@[protected, instance]
def prod.has_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
has_zero (M × N)
Equations
@[simp]
theorem prod.fst_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0.fst = 0
@[simp]
theorem prod.fst_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1.fst = 1
@[simp]
theorem prod.snd_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1.snd = 1
@[simp]
theorem prod.snd_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0.snd = 0
theorem prod.one_eq_mk {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1 = (1, 1)
theorem prod.zero_eq_mk {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0 = (0, 0)
@[simp]
theorem prod.mk_eq_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] {x : M} {y : N} :
(x, y) = 0 x = 0 y = 0
@[simp]
theorem prod.mk_eq_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] {x : M} {y : N} :
(x, y) = 1 x = 1 y = 1
@[simp]
theorem prod.swap_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :
0.swap = 0
@[simp]
theorem prod.swap_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :
1.swap = 1
theorem prod.fst_mul_snd {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (p : M × N) :
(p.fst, 1) * (1, p.snd) = p
theorem prod.fst_add_snd {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (p : M × N) :
(p.fst, 0) + (0, p.snd) = p
@[protected, instance]
def prod.has_neg {M : Type u_5} {N : Type u_6} [has_neg M] [has_neg N] :
has_neg (M × N)
Equations
@[protected, instance]
def prod.has_inv {M : Type u_5} {N : Type u_6} [has_inv M] [has_inv N] :
has_inv (M × N)
Equations
@[simp]
theorem prod.fst_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :
(-p).fst = -p.fst
@[simp]
theorem prod.fst_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :
@[simp]
theorem prod.snd_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :
@[simp]
theorem prod.snd_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :
(-p).snd = -p.snd
@[simp]
theorem prod.inv_mk {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (a : G) (b : H) :
(a, b)⁻¹ = (a⁻¹, b⁻¹)
@[simp]
theorem prod.neg_mk {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (a : G) (b : H) :
-(a, b) = (-a, -b)
@[simp]
theorem prod.swap_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :
(-p).swap = -p.swap
@[simp]
theorem prod.swap_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :
@[protected, instance]
def prod.has_div {M : Type u_5} {N : Type u_6} [has_div M] [has_div N] :
has_div (M × N)
Equations
@[protected, instance]
def prod.has_sub {M : Type u_5} {N : Type u_6} [has_sub M] [has_sub N] :
has_sub (M × N)
Equations
@[simp]
theorem prod.fst_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :
(a / b).fst = a.fst / b.fst
@[simp]
theorem prod.fst_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :
(a - b).fst = a.fst - b.fst
@[simp]
theorem prod.snd_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :
(a / b).snd = a.snd / b.snd
@[simp]
theorem prod.snd_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :
(a - b).snd = a.snd - b.snd
@[simp]
theorem prod.mk_sub_mk {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (x₁ x₂ : G) (y₁ y₂ : H) :
(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
@[simp]
theorem prod.mk_div_mk {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (x₁ x₂ : G) (y₁ y₂ : H) :
(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
@[simp]
theorem prod.swap_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :
(a / b).swap = a.swap / b.swap
@[simp]
theorem prod.swap_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :
(a - b).swap = a.swap - b.swap
@[protected, instance]
def prod.mul_zero_class {M : Type u_5} {N : Type u_6} [mul_zero_class M] [mul_zero_class N] :
Equations
@[protected, instance]
def prod.semigroup {M : Type u_5} {N : Type u_6} [semigroup M] [semigroup N] :
Equations
@[protected, instance]
def prod.add_semigroup {M : Type u_5} {N : Type u_6} [add_semigroup M] [add_semigroup N] :
Equations
@[protected, instance]
def prod.comm_semigroup {G : Type u_3} {H : Type u_4} [comm_semigroup G] [comm_semigroup H] :
Equations
@[protected, instance]
def prod.add_zero_class {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :
Equations
@[protected, instance]
def prod.mul_one_class {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
Equations
@[protected, instance]
def prod.monoid {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
monoid (M × N)
Equations
@[protected, instance]
def prod.add_monoid {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] :
Equations
def mul_hom.fst (M : Type u_5) (N : Type u_6) [has_mul M] [has_mul N] :
M × N →ₙ* M

Given magmas M, N, the natural projection homomorphism from M × N to M.

Equations
def add_hom.fst (M : Type u_5) (N : Type u_6) [has_add M] [has_add N] :
add_hom (M × N) M

Given additive magmas A, B, the natural projection homomorphism from A × B to A

Equations
def add_hom.snd (M : Type u_5) (N : Type u_6) [has_add M] [has_add N] :
add_hom (M × N) N

Given additive magmas A, B, the natural projection homomorphism from A × B to B

Equations
def mul_hom.snd (M : Type u_5) (N : Type u_6) [has_mul M] [has_mul N] :
M × N →ₙ* N

Given magmas M, N, the natural projection homomorphism from M × N to N.

Equations
@[simp]
theorem mul_hom.coe_fst {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :
@[simp]
theorem add_hom.coe_fst {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :
@[simp]
theorem mul_hom.coe_snd {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :
@[simp]
theorem add_hom.coe_snd {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :
@[protected]
def mul_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
M →ₙ* N × P

Combine two monoid_homs f : M →ₙ* N, g : M →ₙ* P into f.prod g : M →ₙ* (N × P) given by (f.prod g) x = (f x, g x).

Equations
@[protected]
def add_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :
add_hom M (N × P)

Combine two add_monoid_homs f : add_hom M N, g : add_hom M P into f.prod g : add_hom M (N × P) given by (f.prod g) x = (f x, g x)

Equations
theorem add_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :
theorem mul_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
@[simp]
theorem add_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
theorem mul_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
theorem mul_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
(mul_hom.fst N P).comp (f.prod g) = f
@[simp]
theorem add_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :
(add_hom.fst N P).comp (f.prod g) = f
@[simp]
theorem add_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :
(add_hom.snd N P).comp (f.prod g) = g
@[simp]
theorem mul_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
(mul_hom.snd N P).comp (f.prod g) = g
@[simp]
theorem add_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M (N × P)) :
((add_hom.fst N P).comp f).prod ((add_hom.snd N P).comp f) = f
@[simp]
theorem mul_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N × P) :
((mul_hom.fst N P).comp f).prod ((mul_hom.snd N P).comp f) = f
def add_hom.prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :
add_hom (M × N) (M' × N')

prod.map as an add_monoid_hom

Equations
def mul_hom.prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
M × N →ₙ* M' × N'

prod.map as a monoid_hom.

Equations
theorem add_hom.prod_map_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :
f.prod_map g = (f.comp (add_hom.fst M N)).prod (g.comp (add_hom.snd M N))
theorem mul_hom.prod_map_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
f.prod_map g = (f.comp (mul_hom.fst M N)).prod (g.comp (mul_hom.snd M N))
@[simp]
theorem add_hom.coe_prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :
@[simp]
theorem mul_hom.coe_prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
theorem mul_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] [has_mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
theorem add_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] [has_add P] (f : add_hom P M) (g : add_hom P N) (f' : add_hom M M') (g' : add_hom N N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def mul_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) :
M × N →ₙ* P

Coproduct of two mul_homs with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2.

Equations
def add_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] (f : add_hom M P) (g : add_hom N P) :
add_hom (M × N) P

Coproduct of two add_homs with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2.

Equations
@[simp]
theorem add_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] (f : add_hom M P) (g : add_hom N P) (p : M × N) :
(f.coprod g) p = f p.fst + g p.snd
@[simp]
theorem mul_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) :
(f.coprod g) p = f p.fst * g p.snd
theorem mul_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] {Q : Type u_1} [comm_semigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem add_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] {Q : Type u_1} [add_comm_semigroup Q] (h : add_hom P Q) (f : add_hom M P) (g : add_hom N P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
def monoid_hom.fst (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :
M × N →* M

Given monoids M, N, the natural projection homomorphism from M × N to M.

Equations
def add_monoid_hom.fst (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :
M × N →+ M

Given additive monoids A, B, the natural projection homomorphism from A × B to A

Equations
def monoid_hom.snd (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :
M × N →* N

Given monoids M, N, the natural projection homomorphism from M × N to N.

Equations
def add_monoid_hom.snd (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :
M × N →+ N

Given additive monoids A, B, the natural projection homomorphism from A × B to B

Equations
def monoid_hom.inl (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :
M →* M × N

Given monoids M, N, the natural inclusion homomorphism from M to M × N.

Equations
def add_monoid_hom.inl (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :
M →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from A to A × B.

Equations
def add_monoid_hom.inr (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :
N →+ M × N

Given additive monoids A, B, the natural inclusion homomorphism from B to A × B.

Equations
def monoid_hom.inr (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :
N →* M × N

Given monoids M, N, the natural inclusion homomorphism from N to M × N.

Equations
@[simp]
theorem monoid_hom.coe_fst {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
@[simp]
@[simp]
@[simp]
theorem monoid_hom.coe_snd {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
@[simp]
theorem monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (x : M) :
(monoid_hom.inl M N) x = (x, 1)
@[simp]
theorem add_monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (x : M) :
(add_monoid_hom.inl M N) x = (x, 0)
@[simp]
theorem monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (y : N) :
(monoid_hom.inr M N) y = (1, y)
@[simp]
theorem add_monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (y : N) :
(add_monoid_hom.inr M N) y = (0, y)
@[simp]
@[simp]
theorem monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
@[simp]
theorem monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
@[simp]
@[protected]
def add_monoid_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :
M →+ N × P

Combine two add_monoid_homs f : M →+ N, g : M →+ P into f.prod g : M →+ N × P given by (f.prod g) x = (f x, g x)

Equations
@[protected]
def monoid_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :
M →* N × P

Combine two monoid_homs f : M →* N, g : M →* P into f.prod g : M →* N × P given by (f.prod g) x = (f x, g x).

Equations
theorem add_monoid_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :
theorem monoid_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :
@[simp]
theorem monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
theorem add_monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
theorem add_monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :
@[simp]
theorem monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :
(monoid_hom.fst N P).comp (f.prod g) = f
@[simp]
theorem add_monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :
@[simp]
theorem monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :
(monoid_hom.snd N P).comp (f.prod g) = g
@[simp]
theorem monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N × P) :
@[simp]
theorem add_monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N × P) :
def add_monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :
M × N →+ M' × N'

prod.map as an add_monoid_hom

Equations
def monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :
M × N →* M' × N'

prod.map as a monoid_hom.

Equations
theorem add_monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :
theorem monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :
@[simp]
theorem monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :
@[simp]
theorem add_monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :
theorem add_monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] [add_zero_class P] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
theorem monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] [mul_one_class P] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :
(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :
M × N →* P

Coproduct of two monoid_homs with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2.

Equations
def add_monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :
M × N →+ P

Coproduct of two add_monoid_homs with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2.

Equations
@[simp]
theorem monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) (p : M × N) :
(f.coprod g) p = f p.fst * g p.snd
@[simp]
theorem add_monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) (p : M × N) :
(f.coprod g) p = f p.fst + g p.snd
@[simp]
theorem add_monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :
@[simp]
theorem monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp (monoid_hom.inl M N) = f
@[simp]
theorem monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp (monoid_hom.inr M N) = g
@[simp]
theorem add_monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :
@[simp]
theorem monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M × N →* P) :
@[simp]
theorem add_monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M × N →+ P) :
@[simp]
theorem add_monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] {Q : Type u_1} [add_comm_monoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] {Q : Type u_1} [comm_monoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
def mul_equiv.prod_comm {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :
M × N ≃* N × M

The equivalence between M × N and N × M given by swapping the components is multiplicative.

Equations
def add_equiv.prod_comm {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :
M × N ≃+ N × M

The equivalence between M × N and N × M given by swapping the components is additive.

Equations
def add_equiv.prod_prod_prod_comm (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] (M' : Type u_8) (N' : Type u_9) [add_zero_class M'] [add_zero_class N'] :
(M × N) × M' × N' ≃+ (M × M') × N × N'

Four-way commutativity of prod. The name matches mul_mul_mul_comm

Equations
@[simp]
theorem add_equiv.prod_prod_prod_comm_apply (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] (M' : Type u_8) (N' : Type u_9) [add_zero_class M'] [add_zero_class N'] (mnmn : (M × N) × M' × N') :
(add_equiv.prod_prod_prod_comm M N M' N') mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)
@[simp]
theorem mul_equiv.prod_prod_prod_comm_apply (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] (mnmn : (M × N) × M' × N') :
(mul_equiv.prod_prod_prod_comm M N M' N') mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)
def mul_equiv.prod_prod_prod_comm (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] :
(M × N) × M' × N' ≃* (M × M') × N × N'

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

Equations
@[simp]
def mul_equiv.prod_congr {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M ≃* M') (g : N ≃* N') :
M × N ≃* M' × N'

Product of multiplicative isomorphisms; the maps come from equiv.prod_congr.

Equations
def add_equiv.prod_congr {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M ≃+ M') (g : N ≃+ N') :
M × N ≃+ M' × N'

Product of additive isomorphisms; the maps come from equiv.prod_congr.

Equations
def add_equiv.unique_prod {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] [unique N] :
N × M ≃+ M

Multiplying by the trivial monoid doesn't change the structure.

Equations
def mul_equiv.unique_prod {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] [unique N] :
N × M ≃* M

Multiplying by the trivial monoid doesn't change the structure.

Equations
def add_equiv.prod_unique {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] [unique N] :
M × N ≃+ M

Multiplying by the trivial monoid doesn't change the structure.

Equations
def mul_equiv.prod_unique {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] [unique N] :
M × N ≃* M

Multiplying by the trivial monoid doesn't change the structure.

Equations

The additive monoid equivalence between additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Equations
def mul_equiv.prod_units {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :
(M × N)ˣ ≃* Mˣ × Nˣ

The monoid equivalence between units of a product of two monoids, and the product of the units of each monoid.

Equations
@[simp]
def units.embed_product (α : Type u_1) [monoid α] :

Canonical homomorphism of monoids from αˣ into α × αᵐᵒᵖ. Used mainly to define the natural topology of αˣ.

Equations

Canonical homomorphism of additive monoids from add_units α into α × αᵃᵒᵖ. Used mainly to define the natural topology of add_units α.

Equations

Multiplication and division as homomorphisms #

@[simp]
theorem mul_mul_hom_apply {α : Type u_8} [comm_semigroup α] (a : α × α) :
@[simp]
theorem add_add_hom_apply {α : Type u_8} [add_comm_semigroup α] (a : α × α) :
def mul_mul_hom {α : Type u_8} [comm_semigroup α] :
α × α →ₙ* α

Multiplication as a multiplicative homomorphism.

Equations
def add_add_hom {α : Type u_8} [add_comm_semigroup α] :
add_hom × α) α

Addition as an additive homomorphism.

Equations
def add_add_monoid_hom {α : Type u_8} [add_comm_monoid α] :
α × α →+ α

Addition as an additive monoid homomorphism.

Equations
@[simp]
theorem mul_monoid_hom_apply {α : Type u_8} [comm_monoid α] (ᾰ : α × α) :
@[simp]
theorem add_add_monoid_hom_apply {α : Type u_8} [add_comm_monoid α] (ᾰ : α × α) :
def mul_monoid_hom {α : Type u_8} [comm_monoid α] :
α × α →* α

Multiplication as a monoid homomorphism.

Equations

Multiplication as a multiplicative homomorphism with zero.

Equations
@[simp]
theorem div_monoid_hom_apply {α : Type u_8} [division_comm_monoid α] (a : α × α) :
def sub_add_monoid_hom {α : Type u_8} [subtraction_comm_monoid α] :
α × α →+ α

Subtraction as an additive monoid homomorphism.

Equations
@[simp]
theorem sub_add_monoid_hom_apply {α : Type u_8} [subtraction_comm_monoid α] (a : α × α) :
def div_monoid_hom {α : Type u_8} [division_comm_monoid α] :
α × α →* α

Division as a monoid homomorphism.

Equations
def div_monoid_with_zero_hom {α : Type u_8} [comm_group_with_zero α] :
α × α →*₀ α

Division as a multiplicative homomorphism with zero.

Equations