# mathlibdocumentation

algebra.group.prod

# Monoid, group etc structures on `M × N`#

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_hom`s:

• `fst M N : M × N →* M`, `snd M N : M × N →* N`: projections `prod.fst` and `prod.snd` as `monoid_hom`s;
• `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid into the product;
• `f.prod g :`M →* N × P`: sends`x`to`(f x, g x)`;
• `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
• `f.prod_map g : M × N → M' × N'`: `prod.map f g` as a `monoid_hom`, sends `(x, y)` to `(f x, g y)`.

## Main declarations #

• `mul_mul_hom`/`mul_monoid_hom`/`mul_monoid_with_zero_hom`: Multiplication bundled as a multiplicative/monoid/monoid with zero homomorphism.
• `div_monoid_hom`/`div_monoid_with_zero_hom`: Division bundled as a monoid/monoid with zero homomorphism.
@[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)
@[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} (p : M × N) :
(p.fst, 1) * (1, p.snd) = p
theorem prod.fst_add_snd {M : Type u_5} {N : Type u_6} (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_involutive_inv {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.has_involutive_neg {M : Type u_5} {N : Type u_6}  :
Equations
@[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}  :
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}  :
Equations
@[protected, instance]
def prod.add_comm_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.comm_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.semigroup_with_zero {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.add_zero_class {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.mul_one_class {M : Type u_5} {N : Type u_6}  :
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
@[protected, instance]
def prod.div_inv_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.sub_neg_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.division_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.subtraction_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.subtraction_comm_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.division_comm_monoid {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.add_group {G : Type u_3} {H : Type u_4} [add_group G] [add_group H] :
Equations
@[protected, instance]
def prod.group {G : Type u_3} {H : Type u_4} [group G] [group H] :
group (G × H)
Equations
@[protected, instance]
def prod.left_cancel_add_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.left_cancel_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.right_cancel_add_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.right_cancel_semigroup {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.left_cancel_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.left_cancel_add_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.right_cancel_add_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.right_cancel_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.cancel_add_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.cancel_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.add_comm_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.comm_monoid {M : Type u_5} {N : Type u_6} [comm_monoid M] [comm_monoid N] :
Equations
@[protected, instance]
def prod.cancel_comm_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.cancel_add_comm_monoid {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.mul_zero_one_class {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.monoid_with_zero {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.comm_monoid_with_zero {M : Type u_5} {N : Type u_6}  :
Equations
@[protected, instance]
def prod.add_comm_group {G : Type u_3} {H : Type u_4}  :
Equations
@[protected, instance]
def prod.comm_group {G : Type u_3} {H : Type u_4} [comm_group G] [comm_group H] :
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_hom`s `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 : N) (g : P) :
(N × P)

Combine two `add_monoid_hom`s `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 : N) (g : P) :
(f.prod g) = g
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) :
(f.prod g) = g
@[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 : N) (g : 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) :
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 : N) (g : P) :
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 : N) (g : P) :
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) :
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 : (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 : M') (g : 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 : M') (g : N') :
f.prod_map g = (f.comp N)).prod (g.comp 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 N)).prod (g.comp 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 : M') (g : 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 : M) (g : N) (f' : M') (g' : 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] (f : M →ₙ* P) (g : N →ₙ* P) :
M × N →ₙ* P

Coproduct of two `mul_hom`s 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] (f : P) (g : P) :
add_hom (M × N) P

Coproduct of two `add_hom`s 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] (f : P) (g : 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] (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] {Q : Type u_1} (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] {Q : Type u_1} (h : Q) (f : P) (g : 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)  :
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)  :
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)  :
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)  :
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)  :
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)  :
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)  :
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)  :
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}  :
@[simp]
theorem add_monoid_hom.coe_fst {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem add_monoid_hom.coe_snd {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem monoid_hom.coe_snd {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} (x : M) :
N) x = (x, 1)
@[simp]
theorem add_monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} (x : M) :
N) x = (x, 0)
@[simp]
theorem monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} (y : N) :
N) y = (1, y)
@[simp]
theorem add_monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} (y : N) :
N) y = (0, y)
@[simp]
theorem monoid_hom.fst_comp_inl {M : Type u_5} {N : Type u_6}  :
N).comp N) =
@[simp]
theorem add_monoid_hom.fst_comp_inl {M : Type u_5} {N : Type u_6}  :
N).comp N) =
@[simp]
theorem add_monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6}  :
N).comp N) = 0
@[simp]
theorem monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6}  :
N).comp N) = 1
@[simp]
theorem add_monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6}  :
N).comp N) = 0
@[simp]
theorem monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6}  :
N).comp N) = 1
@[simp]
theorem add_monoid_hom.snd_comp_inr {M : Type u_5} {N : Type u_6}  :
N).comp N) =
@[simp]
theorem monoid_hom.snd_comp_inr {M : Type u_5} {N : Type u_6}  :
N).comp N) =
@[protected]
def add_monoid_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →+ N) (g : M →+ P) :
M →+ N × P

Combine two `add_monoid_hom`s `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} (f : M →* N) (g : M →* P) :
M →* N × P

Combine two `monoid_hom`s `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} (f : M →+ N) (g : M →+ P) :
(f.prod g) = g
theorem monoid_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →* N) (g : M →* P) :
(f.prod g) = g
@[simp]
theorem monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} (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} (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} (f : M →+ N) (g : M →+ P) :
P).comp (f.prod g) = f
@[simp]
theorem monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →* N) (g : M →* P) :
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} (f : M →+ N) (g : M →+ P) :
P).comp (f.prod g) = g
@[simp]
theorem monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →* N) (g : M →* P) :
P).comp (f.prod g) = g
@[simp]
theorem monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →* N × P) :
P).comp f).prod P).comp f) = f
@[simp]
theorem add_monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →+ N × P) :
P).comp f).prod P).comp f) = f
def add_monoid_hom.prod_map {M : Type u_5} {N : Type u_6} {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} {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} {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :
f.prod_map g = (f.comp N)).prod (g.comp N))
theorem monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :
f.prod_map g = (f.comp N)).prod (g.comp N))
@[simp]
theorem monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} {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} {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} {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (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} {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (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} [comm_monoid P] (f : M →* P) (g : N →* P) :
M × N →* P

Coproduct of two `monoid_hom`s 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} (f : M →+ P) (g : N →+ P) :
M × N →+ P

Coproduct of two `add_monoid_hom`s 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} [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} (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} (f : M →+ P) (g : N →+ P) :
(f.coprod g).comp N) = f
@[simp]
theorem monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp N) = f
@[simp]
theorem monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [comm_monoid P] (f : M →* P) (g : N →* P) :
(f.coprod g).comp N) = g
@[simp]
theorem add_monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M →+ P) (g : N →+ P) :
(f.coprod g).comp N) = g
@[simp]
theorem monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [comm_monoid P] (f : M × N →* P) :
(f.comp N)).coprod (f.comp N)) = f
@[simp]
theorem add_monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} (f : M × N →+ P) :
(f.comp N)).coprod (f.comp N)) = f
@[simp]
theorem add_monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2}  :
@[simp]
theorem monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [comm_monoid M] [comm_monoid N] :
N).coprod N) = monoid_hom.id (M × N)
theorem add_monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_1} (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} [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}  :
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}  :
M × N ≃+ N × M

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

Equations
@[simp]
theorem add_equiv.coe_prod_comm {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem mul_equiv.coe_prod_comm {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem add_equiv.coe_prod_comm_symm {M : Type u_5} {N : Type u_6}  :
@[simp]
theorem mul_equiv.coe_prod_comm_symm {M : Type u_5} {N : Type u_6}  :
def mul_equiv.prod_congr {M : Type u_5} {N : Type u_6} {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} {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} [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} [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} [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} [unique N] :
M × N ≃* M

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

Equations
def add_equiv.prod_add_units {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] :

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]
theorem units.embed_product_apply (α : Type u_1) [monoid α] (x : αˣ) :
x = (x,
def units.embed_product (α : Type u_1) [monoid α] :

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

Equations
def add_units.embed_product (α : Type u_1) [add_monoid α] :

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

Equations
@[simp]
theorem add_units.embed_product_apply (α : Type u_1) [add_monoid α] (x : add_units α) :
= (x,
theorem add_units.embed_product_injective (α : Type u_1) [add_monoid α] :
theorem units.embed_product_injective (α : Type u_1) [monoid α] :

### Multiplication and division as homomorphisms #

@[simp]
theorem mul_mul_hom_apply {α : Type u_8} (a : α × α) :
= a.fst * a.snd
@[simp]
theorem add_add_hom_apply {α : Type u_8} (a : α × α) :
= a.fst + a.snd
def mul_mul_hom {α : Type u_8}  :
α × α →ₙ* α

Multiplication as a multiplicative homomorphism.

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

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

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

Multiplication as a monoid homomorphism.

Equations
def mul_monoid_with_zero_hom {α : Type u_8}  :
α × α →*₀ α

Multiplication as a multiplicative homomorphism with zero.

Equations
@[simp]
theorem mul_monoid_with_zero_hom_apply {α : Type u_8} (ᾰ : α × α) :
@[simp]
theorem div_monoid_hom_apply {α : Type u_8} (a : α × α) :
= a.fst / a.snd
def sub_add_monoid_hom {α : Type u_8}  :
α × α →+ α

Subtraction as an additive monoid homomorphism.

Equations
@[simp]
theorem sub_add_monoid_hom_apply {α : Type u_8} (a : α × α) :
= a.fst - a.snd
def div_monoid_hom {α : Type u_8}  :
α × α →* α

Division as a monoid homomorphism.

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

Division as a multiplicative homomorphism with zero.

Equations
@[simp]
theorem div_monoid_with_zero_hom_apply {α : Type u_8} (a : α × α) :