# 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 MonoidHoms:

• fst M N : M × N →* M, snd M N : M × N →* N: projections Prod.fst and Prod.snd as MonoidHoms;
• 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);
• When P is commutative, f.coprod g : M × N →* P sends (x, y) to f x * g y (without the commutativity assumption on P, see MonoidHom.noncommPiCoprod);
• f.prodMap g : M × N → M' × N': prod.map f g as a MonoidHom, sends (x, y) to (f x, g y).

## Main declarations #

• mulMulHom/mulMonoidHom: Multiplication bundled as a multiplicative/monoid homomorphism.
• divMonoidHom: Division bundled as a monoid homomorphism.
Equations
• Prod.instAdd = { add := fun (p q : M × N) => (p.1 + q.1, p.2 + q.2) }
instance Prod.instMul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] :
Mul (M × N)
Equations
• Prod.instMul = { mul := fun (p q : M × N) => (p.1 * q.1, p.2 * q.2) }
@[simp]
theorem Prod.fst_add {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) :
(p + q).1 = p.1 + q.1
@[simp]
theorem Prod.fst_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) :
(p * q).1 = p.1 * q.1
@[simp]
theorem Prod.snd_add {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) :
(p + q).2 = p.2 + q.2
@[simp]
theorem Prod.snd_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) :
(p * q).2 = p.2 * q.2
@[simp]
theorem Prod.mk_add_mk {M : Type u_5} {N : Type u_6} [Add M] [Add N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :
(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
@[simp]
theorem Prod.mk_mul_mk {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :
(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
@[simp]
theorem Prod.swap_add {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) :
(p + q).swap = p.swap + q.swap
@[simp]
theorem Prod.swap_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) :
(p * q).swap = p.swap * q.swap
theorem Prod.add_def {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) :
p + q = (p.1 + q.1, p.2 + q.2)
theorem Prod.mul_def {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) :
p * q = (p.1 * q.1, p.2 * q.2)
theorem Prod.zero_mk_add_zero_mk {M : Type u_5} {N : Type u_6} [] [Add N] (b₁ : N) (b₂ : N) :
(0, b₁) + (0, b₂) = (0, b₁ + b₂)
theorem Prod.one_mk_mul_one_mk {M : Type u_5} {N : Type u_6} [] [Mul N] (b₁ : N) (b₂ : N) :
(1, b₁) * (1, b₂) = (1, b₁ * b₂)
theorem Prod.mk_zero_add_mk_zero {M : Type u_5} {N : Type u_6} [Add M] [] (a₁ : M) (a₂ : M) :
(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
theorem Prod.mk_one_mul_mk_one {M : Type u_5} {N : Type u_6} [Mul M] [] (a₁ : M) (a₂ : M) :
(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
instance Prod.instZero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] :
Zero (M × N)
Equations
• Prod.instZero = { zero := (0, 0) }
instance Prod.instOne {M : Type u_5} {N : Type u_6} [One M] [One N] :
One (M × N)
Equations
• Prod.instOne = { one := (1, 1) }
@[simp]
theorem Prod.fst_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] :
0.1 = 0
@[simp]
theorem Prod.fst_one {M : Type u_5} {N : Type u_6} [One M] [One N] :
1.1 = 1
@[simp]
theorem Prod.snd_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] :
0.2 = 0
@[simp]
theorem Prod.snd_one {M : Type u_5} {N : Type u_6} [One M] [One N] :
1.2 = 1
theorem Prod.zero_eq_mk {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] :
0 = (0, 0)
theorem Prod.one_eq_mk {M : Type u_5} {N : Type u_6} [One M] [One N] :
1 = (1, 1)
@[simp]
theorem Prod.mk_eq_zero {M : Type u_5} {N : Type u_6} [Zero M] [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} [One M] [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} [Zero M] [Zero N] :
= 0
@[simp]
theorem Prod.swap_one {M : Type u_5} {N : Type u_6} [One M] [One N] :
= 1
theorem Prod.fst_add_snd {M : Type u_5} {N : Type u_6} [] [] (p : M × N) :
(p.1, 0) + (0, p.2) = p
theorem Prod.fst_mul_snd {M : Type u_5} {N : Type u_6} [] [] (p : M × N) :
(p.1, 1) * (1, p.2) = p
instance Prod.instNeg {M : Type u_5} {N : Type u_6} [Neg M] [Neg N] :
Neg (M × N)
Equations
• Prod.instNeg = { neg := fun (p : M × N) => (-p.1, -p.2) }
instance Prod.instInv {M : Type u_5} {N : Type u_6} [Inv M] [Inv N] :
Inv (M × N)
Equations
• Prod.instInv = { inv := fun (p : M × N) => (p.1⁻¹, p.2⁻¹) }
@[simp]
theorem Prod.fst_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) :
(-p).1 = -p.1
@[simp]
theorem Prod.fst_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) :
p⁻¹.1 = p.1⁻¹
@[simp]
theorem Prod.snd_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) :
(-p).2 = -p.2
@[simp]
theorem Prod.snd_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) :
p⁻¹.2 = p.2⁻¹
@[simp]
theorem Prod.neg_mk {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (a : G) (b : H) :
-(a, b) = (-a, -b)
@[simp]
theorem Prod.inv_mk {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (a : G) (b : H) :
(a, b)⁻¹ = (a⁻¹, b⁻¹)
@[simp]
theorem Prod.swap_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) :
(-p).swap = -p.swap
@[simp]
theorem Prod.swap_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) :
p⁻¹.swap = p.swap⁻¹
instance Prod.instInvolutiveNeg {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instInvolutiveNeg =
theorem Prod.instInvolutiveNeg.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x : M × N), - -x = x
instance Prod.instInvolutiveInv {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instInvolutiveInv =
instance Prod.instSub {M : Type u_5} {N : Type u_6} [Sub M] [Sub N] :
Sub (M × N)
Equations
• Prod.instSub = { sub := fun (p q : M × N) => (p.1 - q.1, p.2 - q.2) }
instance Prod.instDiv {M : Type u_5} {N : Type u_6} [Div M] [Div N] :
Div (M × N)
Equations
• Prod.instDiv = { div := fun (p q : M × N) => (p.1 / q.1, p.2 / q.2) }
@[simp]
theorem Prod.fst_sub {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) :
(a - b).1 = a.1 - b.1
@[simp]
theorem Prod.fst_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) :
(a / b).1 = a.1 / b.1
@[simp]
theorem Prod.snd_sub {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) :
(a - b).2 = a.2 - b.2
@[simp]
theorem Prod.snd_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) :
(a / b).2 = a.2 / b.2
@[simp]
theorem Prod.mk_sub_mk {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :
(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
@[simp]
theorem Prod.mk_div_mk {G : Type u_3} {H : Type u_4} [Div G] [Div H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :
(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
@[simp]
theorem Prod.swap_sub {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) :
(a - b).swap = a.swap - b.swap
@[simp]
theorem Prod.swap_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) :
(a / b).swap = a.swap / b.swap
instance Prod.instAddSemigroup {M : Type u_5} {N : Type u_6} [] [] :
Equations
theorem Prod.instAddSemigroup.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x x_1 x_2 : M × N), ((x + x_1).1 + x_2.1, (x + x_1).2 + x_2.2) = (x.1 + (x_1 + x_2).1, x.2 + (x_1 + x_2).2)
instance Prod.instSemigroup {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instSemigroup =
instance Prod.instAddCommSemigroup {G : Type u_3} {H : Type u_4} [] [] :
Equations
theorem Prod.instAddCommSemigroup.proof_1 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x x_1 : G × H), (x.1 + x_1.1, x.2 + x_1.2) = (x_1.1 + x.1, x_1.2 + x.2)
instance Prod.instCommSemigroup {G : Type u_3} {H : Type u_4} [] [] :
Equations
• Prod.instCommSemigroup =
theorem Prod.instAddZeroClass.proof_1 {M : Type u_1} {N : Type u_2} [] [] (a : M × N) :
0 + a = a
theorem Prod.instAddZeroClass.proof_2 {M : Type u_1} {N : Type u_2} [] [] (a : M × N) :
a + 0 = a
instance Prod.instAddZeroClass {M : Type u_5} {N : Type u_6} [] [] :
Equations
instance Prod.instMulOneClass {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instMulOneClass =
theorem Prod.instAddMonoid.proof_4 {M : Type u_1} {N : Type u_2} [] [] (z : ) (a : M × N) :
(fun (z : ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) (z + 1) a = (fun (z : ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) z a + a
theorem Prod.instAddMonoid.proof_1 {M : Type u_1} {N : Type u_2} [] [] (a : M × N) :
0 + a = a
theorem Prod.instAddMonoid.proof_2 {M : Type u_1} {N : Type u_2} [] [] (a : M × N) :
a + 0 = a
instance Prod.instAddMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
theorem Prod.instAddMonoid.proof_3 {M : Type u_1} {N : Type u_2} [] [] (z : M × N) :
(fun (z : ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) 0 z = 0
instance Prod.instMonoid {M : Type u_5} {N : Type u_6} [] [] :
Monoid (M × N)
Equations
instance Prod.subNegMonoid {G : Type u_3} {H : Type u_4} [] [] :
Equations
theorem Prod.subNegMonoid.proof_1 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x x_1 : G × H), (x.1 - x_1.1, x.2 - x_1.2) = (x.1 + (-x_1).1, x.2 + (-x_1).2)
theorem Prod.subNegMonoid.proof_3 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x : ) (x_1 : G × H), (fun (z : ) (a : G × H) => (, )) (Int.ofNat x.succ) x_1 = (fun (z : ) (a : G × H) => (, )) () x_1 + x_1
theorem Prod.subNegMonoid.proof_4 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x : ) (x_1 : G × H), (fun (z : ) (a : G × H) => (, )) () x_1 = -(fun (z : ) (a : G × H) => (, )) (x.succ) x_1
theorem Prod.subNegMonoid.proof_2 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x : G × H), (fun (z : ) (a : G × H) => (, )) 0 x = 0
instance Prod.instDivInvMonoid {G : Type u_3} {H : Type u_4} [] [] :
Equations
instance Prod.instDivisionAddMonoid {G : Type u_3} {H : Type u_4} :
Equations
theorem Prod.instDivisionAddMonoid.proof_1 {G : Type u_1} {H : Type u_2} (a : G × H) :
- -a = a
theorem Prod.instDivisionAddMonoid.proof_3 {G : Type u_1} {H : Type u_2} (a : G × H) (b : G × H) (h : a + b = 0) :
-a = b
theorem Prod.instDivisionAddMonoid.proof_2 {G : Type u_1} {H : Type u_2} (a : G × H) (b : G × H) :
-(a + b) = -b + -a
instance Prod.instDivisionMonoid {G : Type u_3} {H : Type u_4} [] [] :
Equations
• Prod.instDivisionMonoid =
theorem Prod.SubtractionCommMonoid.proof_1 {G : Type u_1} {H : Type u_2} :
∀ (x x_1 : G × H), x + x_1 = x_1 + x
instance Prod.SubtractionCommMonoid {G : Type u_3} {H : Type u_4} :
Equations
• Prod.SubtractionCommMonoid =
abbrev Prod.SubtractionCommMonoid.match_1 {G : Type u_1} {H : Type u_2} (motive : G × HProp) :
∀ (x : G × H), (∀ (fst : G) (snd : H), motive (fst, snd))motive x
Equations
• =
Instances For
instance Prod.instDivisionCommMonoid {G : Type u_3} {H : Type u_4} :
Equations
• Prod.instDivisionCommMonoid =
instance Prod.instAddGroup {G : Type u_3} {H : Type u_4} [] [] :
Equations
theorem Prod.instAddGroup.proof_1 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x : G × H), ((-x).1 + x.1, (-x).2 + x.2) = (0, 0)
instance Prod.instGroup {G : Type u_3} {H : Type u_4} [] [] :
Group (G × H)
Equations
• Prod.instGroup =
instance Prod.instIsAddLeftCancel {G : Type u_3} {H : Type u_4} [Add G] [Add H] [] [] :
Equations
• =
instance Prod.instIsLeftCancelMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [] [] :
Equations
• =
instance Prod.instIsAddRightCancel {G : Type u_3} {H : Type u_4} [Add G] [Add H] [] [] :
Equations
• =
instance Prod.instIsRightCancelMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [] [] :
Equations
• =
instance Prod.instIsAddCancel {G : Type u_3} {H : Type u_4} [Add G] [Add H] [] [] :
Equations
• =
instance Prod.instIsCancelMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [] [] :
Equations
• =
Equations
theorem Prod.instAddLeftCancelSemigroup.proof_1 {G : Type u_1} {H : Type u_2} :
∀ (x x_1 x_2 : G × H), x + x_1 = x + x_2x_1 = x_2
instance Prod.instLeftCancelSemigroup {G : Type u_3} {H : Type u_4} :
Equations
• Prod.instLeftCancelSemigroup =
Equations
theorem Prod.instAddRightCancelSemigroup.proof_1 {G : Type u_1} {H : Type u_2} :
∀ (x x_1 x_2 : G × H), x + x_1 = x_2 + x_1x = x_2
instance Prod.instRightCancelSemigroup {G : Type u_3} {H : Type u_4} :
Equations
• Prod.instRightCancelSemigroup =
theorem Prod.instAddLeftCancelMonoid.proof_4 {M : Type u_1} {N : Type u_2} :
∀ (n : ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x
instance Prod.instAddLeftCancelMonoid {M : Type u_5} {N : Type u_6} :
Equations
theorem Prod.instAddLeftCancelMonoid.proof_1 {M : Type u_1} {N : Type u_2} (a : M × N) :
0 + a = a
theorem Prod.instAddLeftCancelMonoid.proof_3 {M : Type u_1} {N : Type u_2} :
∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x
theorem Prod.instAddLeftCancelMonoid.proof_2 {M : Type u_1} {N : Type u_2} (a : M × N) :
a + 0 = a
instance Prod.instLeftCancelMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
instance Prod.instAddRightCancelMonoid {M : Type u_5} {N : Type u_6} :
Equations
theorem Prod.instAddRightCancelMonoid.proof_2 {M : Type u_1} {N : Type u_2} (a : M × N) :
a + 0 = a
theorem Prod.instAddRightCancelMonoid.proof_4 {M : Type u_1} {N : Type u_2} :
∀ (n : ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem Prod.instAddRightCancelMonoid.proof_3 {M : Type u_1} {N : Type u_2} :
∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x
theorem Prod.instAddRightCancelMonoid.proof_1 {M : Type u_1} {N : Type u_2} (a : M × N) :
0 + a = a
instance Prod.instRightCancelMonoid {M : Type u_5} {N : Type u_6} :
Equations
instance Prod.instAddCancelMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
theorem Prod.instAddCancelMonoid.proof_1 {M : Type u_1} {N : Type u_2} [] [] (a : M × N) (a : M × N) (a : M × N) :
a✝¹ + a✝ = a + a✝a✝¹ = a
instance Prod.instCancelMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instCancelMonoid =
theorem Prod.instAddCommMonoid.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x x_1 : M × N), x + x_1 = x_1 + x
instance Prod.instAddCommMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
instance Prod.instCommMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instCommMonoid =
instance Prod.instAddCancelCommMonoid {M : Type u_5} {N : Type u_6} :
Equations
theorem Prod.instAddCancelCommMonoid.proof_1 {M : Type u_1} {N : Type u_2} :
∀ (x x_1 : M × N), x + x_1 = x_1 + x
instance Prod.instCancelCommMonoid {M : Type u_5} {N : Type u_6} [] [] :
Equations
• Prod.instCancelCommMonoid =
theorem Prod.instAddCommGroup.proof_1 {G : Type u_1} {H : Type u_2} [] [] :
∀ (x x_1 : G × H), x + x_1 = x_1 + x
instance Prod.instAddCommGroup {G : Type u_3} {H : Type u_4} [] [] :
Equations
instance Prod.instCommGroup {G : Type u_3} {H : Type u_4} [] [] :
Equations
• Prod.instCommGroup =
theorem AddSemiconjBy.prod {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} {z : M × N} (hm : AddSemiconjBy x.1 y.1 z.1) (hn : AddSemiconjBy x.2 y.2 z.2) :
theorem SemiconjBy.prod {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) :
theorem Prod.addSemiconjBy_iff {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} {z : M × N} :
theorem Prod.semiconjBy_iff {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} :
SemiconjBy x y z SemiconjBy x.1 y.1 z.1 SemiconjBy x.2 y.2 z.2
theorem AddCommute.prod {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} (hm : AddCommute x.1 y.1) (hn : AddCommute x.2 y.2) :
theorem Commute.prod {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) :
theorem Prod.addCommute_iff {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} :
theorem Prod.commute_iff {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} :
Commute x y Commute x.1 y.1 Commute x.2 y.2
∀ (x x_1 : M × N), (x + x_1).1 = (x + x_1).1

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

Equations
• = { toFun := Prod.fst, map_add' := }
Instances For
def MulHom.fst (M : Type u_5) (N : Type u_6) [Mul M] [Mul N] :
M × N →ₙ* M

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

Equations
• = { toFun := Prod.fst, map_mul' := }
Instances For

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

Equations
• = { toFun := Prod.snd, map_add' := }
Instances For
∀ (x x_1 : M × N), (x + x_1).2 = (x + x_1).2
def MulHom.snd (M : Type u_5) (N : Type u_6) [Mul M] [Mul N] :
M × N →ₙ* N

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

Equations
• = { toFun := Prod.snd, map_mul' := }
Instances For
@[simp]
() = Prod.fst
@[simp]
theorem MulHom.coe_fst {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] :
() = Prod.fst
@[simp]
() = Prod.snd
@[simp]
theorem MulHom.coe_snd {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] :
() = Prod.snd

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

Equations
• f.prod g = { toFun := Pi.prod f g, map_add' := }
Instances For
theorem AddHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) (x : M) (y : M) :
Pi.prod (f) (g) (x + y) = Pi.prod (f) (g) x + Pi.prod (f) (g) y
def MulHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
M →ₙ* N × P

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

Equations
• f.prod g = { toFun := Pi.prod f g, map_mul' := }
Instances For
(f.prod g) = Pi.prod f g
theorem MulHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
(f.prod g) = Pi.prod f g
@[simp]
theorem AddHom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
theorem MulHom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) :
(f.prod g) x = (f x, g x)
@[simp]
().comp (f.prod g) = f
@[simp]
theorem MulHom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
().comp (f.prod g) = f
@[simp]
().comp (f.prod g) = g
@[simp]
theorem MulHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :
().comp (f.prod g) = g
@[simp]
theorem AddHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [Add P] (f : AddHom M (N × P)) :
(().comp f).prod (().comp f) = f
@[simp]
theorem MulHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N × P) :
(().comp f).prod (().comp f) = f
AddHom (M × N) (M' × N')

Prod.map as an AddMonoidHom

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
def MulHom.prodMap {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
M × N →ₙ* M' × N'

Prod.map as a MonoidHom.

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
f.prodMap g = (f.comp ()).prod (g.comp ())
theorem MulHom.prodMap_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
f.prodMap g = (f.comp ()).prod (g.comp ())
@[simp]
(f.prodMap g) = Prod.map f g
@[simp]
theorem MulHom.coe_prodMap {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :
(f.prodMap g) = Prod.map f g
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
theorem MulHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] [Mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def AddHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [] (f : AddHom M P) (g : AddHom N P) :

Coproduct of two AddHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2. (Commutative codomain; for the general case, see AddHom.noncommCoprod)

Equations
• f.coprod g = f.comp () + g.comp ()
Instances For
def MulHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [] (f : M →ₙ* P) (g : N →ₙ* P) :
M × N →ₙ* P

Coproduct of two MulHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative codomain; for the general case, see MulHom.noncommCoprod)

Equations
• f.coprod g = f.comp () * g.comp ()
Instances For
@[simp]
theorem AddHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [] (f : AddHom M P) (g : AddHom N P) (p : M × N) :
(f.coprod g) p = f p.1 + g p.2
@[simp]
theorem MulHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) :
(f.coprod g) p = f p.1 * g p.2
theorem AddHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [] {Q : Type u_8} [] (h : AddHom P Q) (f : AddHom M P) (g : AddHom N P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem MulHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [] {Q : Type u_8} [] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem AddMonoidHom.fst.proof_2 (M : Type u_1) (N : Type u_2) [] [] :
∀ (x x_1 : M × N), { toFun := Prod.fst, map_zero' := }.toFun (x + x_1) = { toFun := Prod.fst, map_zero' := }.toFun (x + x_1)
theorem AddMonoidHom.fst.proof_1 (M : Type u_1) (N : Type u_2) [] [] :
0.1 = 0.1
def AddMonoidHom.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
• = { toFun := Prod.fst, map_zero' := , map_add' := }
Instances For
def MonoidHom.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
• = { toFun := Prod.fst, map_one' := , map_mul' := }
Instances For
def AddMonoidHom.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
• = { toFun := Prod.snd, map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.snd.proof_2 (M : Type u_1) (N : Type u_2) [] [] :
∀ (x x_1 : M × N), { toFun := Prod.snd, map_zero' := }.toFun (x + x_1) = { toFun := Prod.snd, map_zero' := }.toFun (x + x_1)
theorem AddMonoidHom.snd.proof_1 (M : Type u_2) (N : Type u_1) [] [] :
0.2 = 0.2
def MonoidHom.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
• = { toFun := Prod.snd, map_one' := , map_mul' := }
Instances For
def AddMonoidHom.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
• = { toFun := fun (x : M) => (x, 0), map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.inl.proof_1 (M : Type u_1) (N : Type u_2) [] [] :
(fun (x : M) => (x, 0)) 0 = (fun (x : M) => (x, 0)) 0
theorem AddMonoidHom.inl.proof_2 (M : Type u_2) (N : Type u_1) [] [] :
∀ (x x_1 : M), { toFun := fun (x : M) => (x, 0), map_zero' := }.toFun (x + x_1) = { toFun := fun (x : M) => (x, 0), map_zero' := }.toFun x + { toFun := fun (x : M) => (x, 0), map_zero' := }.toFun x_1
def MonoidHom.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
• = { toFun := fun (x : M) => (x, 1), map_one' := , map_mul' := }
Instances For
theorem AddMonoidHom.inr.proof_1 (M : Type u_1) (N : Type u_2) [] [] :
(fun (y : N) => (0, y)) 0 = (fun (y : N) => (0, y)) 0
theorem AddMonoidHom.inr.proof_2 (M : Type u_2) (N : Type u_1) [] [] :
∀ (x x_1 : N), { toFun := fun (y : N) => (0, y), map_zero' := }.toFun (x + x_1) = { toFun := fun (y : N) => (0, y), map_zero' := }.toFun x + { toFun := fun (y : N) => (0, y), map_zero' := }.toFun x_1
def AddMonoidHom.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
• = { toFun := fun (y : N) => (0, y), map_zero' := , map_add' := }
Instances For
def MonoidHom.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
• = { toFun := fun (y : N) => (1, y), map_one' := , map_mul' := }
Instances For
@[simp]
theorem AddMonoidHom.coe_fst {M : Type u_5} {N : Type u_6} [] [] :
() = Prod.fst
@[simp]
theorem MonoidHom.coe_fst {M : Type u_5} {N : Type u_6} [] [] :
() = Prod.fst
@[simp]
theorem AddMonoidHom.coe_snd {M : Type u_5} {N : Type u_6} [] [] :
() = Prod.snd
@[simp]
theorem MonoidHom.coe_snd {M : Type u_5} {N : Type u_6} [] [] :
() = Prod.snd
@[simp]
theorem AddMonoidHom.inl_apply {M : Type u_5} {N : Type u_6} [] [] (x : M) :
() x = (x, 0)
@[simp]
theorem MonoidHom.inl_apply {M : Type u_5} {N : Type u_6} [] [] (x : M) :
() x = (x, 1)
@[simp]
theorem AddMonoidHom.inr_apply {M : Type u_5} {N : Type u_6} [] [] (y : N) :
() y = (0, y)
@[simp]
theorem MonoidHom.inr_apply {M : Type u_5} {N : Type u_6} [] [] (y : N) :
() y = (1, y)
@[simp]
theorem AddMonoidHom.fst_comp_inl {M : Type u_5} {N : Type u_6} [] [] :
().comp () =
@[simp]
theorem MonoidHom.fst_comp_inl {M : Type u_5} {N : Type u_6} [] [] :
().comp () =
@[simp]
theorem AddMonoidHom.snd_comp_inl {M : Type u_5} {N : Type u_6} [] [] :
().comp () = 0
@[simp]
theorem MonoidHom.snd_comp_inl {M : Type u_5} {N : Type u_6} [] [] :
().comp () = 1
@[simp]
theorem AddMonoidHom.fst_comp_inr {M : Type u_5} {N : Type u_6} [] [] :
().comp () = 0
@[simp]
theorem MonoidHom.fst_comp_inr {M : Type u_5} {N : Type u_6} [] [] :
().comp () = 1
@[simp]
theorem AddMonoidHom.snd_comp_inr {M : Type u_5} {N : Type u_6} [] [] :
().comp () =
@[simp]
theorem MonoidHom.snd_comp_inr {M : Type u_5} {N : Type u_6} [] [] :
().comp () =
theorem AddMonoidHom.addCommute_inl_inr {M : Type u_5} {N : Type u_6} [] [] (m : M) (n : N) :
theorem MonoidHom.commute_inl_inr {M : Type u_5} {N : Type u_6} [] [] (m : M) (n : N) :
Commute (() m) (() n)
def AddMonoidHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →+ N) (g : M →+ P) :
M →+ N × P

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

Equations
• f.prod g = { toFun := Pi.prod f g, map_zero' := , map_add' := }
Instances For
theorem AddMonoidHom.prod.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [] [] [] (f : M →+ N) (g : M →+ P) (x : M) (y : M) :
{ toFun := Pi.prod f g, map_zero' := }.toFun (x + y) = { toFun := Pi.prod f g, map_zero' := }.toFun x + { toFun := Pi.prod f g, map_zero' := }.toFun y
theorem AddMonoidHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [] [] [] (f : M →+ N) (g : M →+ P) :
Pi.prod (f) (g) 0 = 0
def MonoidHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →* N) (g : M →* P) :
M →* N × P

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

Equations
• f.prod g = { toFun := Pi.prod f g, map_one' := , map_mul' := }
Instances For
theorem AddMonoidHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →+ N) (g : M →+ P) :
(f.prod g) = Pi.prod f g
theorem MonoidHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →* N) (g : M →* P) :
(f.prod g) = Pi.prod f g
@[simp]
theorem AddMonoidHom.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 MonoidHom.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 AddMonoidHom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →+ N) (g : M →+ P) :
().comp (f.prod g) = f
@[simp]
theorem MonoidHom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →* N) (g : M →* P) :
().comp (f.prod g) = f
@[simp]
theorem AddMonoidHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →+ N) (g : M →+ P) :
().comp (f.prod g) = g
@[simp]
theorem MonoidHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →* N) (g : M →* P) :
().comp (f.prod g) = g
@[simp]
theorem AddMonoidHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →+ N × P) :
(().comp f).prod (().comp f) = f
@[simp]
theorem MonoidHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M →* N × P) :
(().comp f).prod (().comp f) = f
def AddMonoidHom.prodMap {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →+ M') (g : N →+ N') :
M × N →+ M' × N'

prod.map as an AddMonoidHom.

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
def MonoidHom.prodMap {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →* M') (g : N →* N') :
M × N →* M' × N'

prod.map as a MonoidHom.

Equations
• f.prodMap g = (f.comp ()).prod (g.comp ())
Instances For
theorem AddMonoidHom.prodMap_def {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →+ M') (g : N →+ N') :
f.prodMap g = (f.comp ()).prod (g.comp ())
theorem MonoidHom.prodMap_def {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →* M') (g : N →* N') :
f.prodMap g = (f.comp ()).prod (g.comp ())
@[simp]
theorem AddMonoidHom.coe_prodMap {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →+ M') (g : N →+ N') :
(f.prodMap g) = Prod.map f g
@[simp]
theorem MonoidHom.coe_prodMap {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M →* M') (g : N →* N') :
(f.prodMap g) = Prod.map f g
theorem AddMonoidHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] {M' : Type u_8} {N' : Type u_9} [] [] [] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
theorem MonoidHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] {M' : Type u_8} {N' : Type u_9} [] [] [] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :
(f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
def AddMonoidHom.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 AddMonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2. (Commutative case; for the general case, see AddHom.noncommCoprod.)

Equations
• f.coprod g = f.comp () + g.comp ()
Instances For
def MonoidHom.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 MonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative case; for the general case, see MonoidHom.noncommCoprod.)

Equations
• f.coprod g = f.comp () * g.comp ()
Instances For
@[simp]
theorem AddMonoidHom.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.1 + g p.2
@[simp]
theorem MonoidHom.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.1 * g p.2
@[simp]
theorem AddMonoidHom.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 () = f
@[simp]
theorem MonoidHom.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 () = f
@[simp]
theorem AddMonoidHom.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 () = g
@[simp]
theorem MonoidHom.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 () = g
@[simp]
theorem AddMonoidHom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M × N →+ P) :
(f.comp ()).coprod (f.comp ()) = f
@[simp]
theorem MonoidHom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] (f : M × N →* P) :
(f.comp ()).coprod (f.comp ()) = f
@[simp]
theorem AddMonoidHom.coprod_inl_inr {M : Type u_8} {N : Type u_9} [] [] :
().coprod () = AddMonoidHom.id (M × N)
@[simp]
theorem MonoidHom.coprod_inl_inr {M : Type u_8} {N : Type u_9} [] [] :
().coprod () = MonoidHom.id (M × N)
theorem AddMonoidHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] {Q : Type u_8} [] (h : P →+ Q) (f : M →+ P) (g : N →+ P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem MonoidHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [] [] [] {Q : Type u_8} [] (h : P →* Q) (f : M →* P) (g : N →* P) :
h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)
theorem AddEquiv.prodComm.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x x_1 : M × N), ().toFun (x + x_1) = ().toFun x + ().toFun x_1
def AddEquiv.prodComm {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
• AddEquiv.prodComm = let __src := ; { toEquiv := __src, map_add' := }
Instances For
def MulEquiv.prodComm {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
• MulEquiv.prodComm = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
@[simp]
theorem AddEquiv.coe_prodComm {M : Type u_5} {N : Type u_6} [] [] :
@[simp]
theorem MulEquiv.coe_prodComm {M : Type u_5} {N : Type u_6} [] [] :
MulEquiv.prodComm = Prod.swap
@[simp]
theorem AddEquiv.coe_prodComm_symm {M : Type u_5} {N : Type u_6} [] [] :
@[simp]
theorem MulEquiv.coe_prodComm_symm {M : Type u_5} {N : Type u_6} [] [] :
MulEquiv.prodComm.symm = Prod.swap
theorem AddEquiv.prodProdProdComm.proof_2 (M : Type u_1) (N : Type u_2) (M' : Type u_3) (N' : Type u_4) :
theorem AddEquiv.prodProdProdComm.proof_1 (M : Type u_1) (N : Type u_2) (M' : Type u_3) (N' : Type u_4) :
def AddEquiv.prodProdProdComm (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] :
(M × N) × M' × N' ≃+ (M × M') × N × N'

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
theorem AddEquiv.prodProdProdComm.proof_3 (M : Type u_2) (N : Type u_1) [] [] (M' : Type u_4) (N' : Type u_3) [] [] (_mnmn : (M × N) × M' × N') (_mnmn' : (M × N) × M' × N') :
{ toFun := fun (mnmn : (M × N) × M' × N') => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2), invFun := fun (mmnn : (M × M') × N × N') => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := , right_inv := }.toFun (_mnmn + _mnmn') = { toFun := fun (mnmn : (M × N) × M' × N') => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2), invFun := fun (mmnn : (M × M') × N × N') => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := , right_inv := }.toFun (_mnmn + _mnmn')
@[simp]
theorem MulEquiv.prodProdProdComm_apply (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] (mnmn : (M × N) × M' × N') :
() mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
@[simp]
theorem AddEquiv.prodProdProdComm_apply (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] (mnmn : (M × N) × M' × N') :
() mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
def MulEquiv.prodProdProdComm (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] :
(M × N) × M' × N' ≃* (M × M') × N × N'

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddEquiv.prodProdProdComm_toEquiv (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] :
() = Equiv.prodProdProdComm M N M' N'
@[simp]
theorem MulEquiv.prodProdProdComm_toEquiv (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] :
() = Equiv.prodProdProdComm M N M' N'
@[simp]
theorem MulEquiv.prodProdProdComm_symm (M : Type u_5) (N : Type u_6) [] [] (M' : Type u_8) (N' : Type u_9) [] [] :
().symm =
theorem AddEquiv.prodCongr.proof_1 {M : Type u_1} {N : Type u_2} [] [] {M' : Type u_4} {N' : Type u_3} [] [] (f : M ≃+ M') (g : N ≃+ N') :
∀ (x x_1 : M × N), (f.prodCongr g.toEquiv).toFun (x + x_1) = (f.prodCongr g.toEquiv).toFun x + (f.prodCongr g.toEquiv).toFun x_1
def AddEquiv.prodCongr {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M ≃+ M') (g : N ≃+ N') :
M × N ≃+ M' × N'

Product of additive isomorphisms; the maps come from Equiv.prodCongr.

Equations
• f.prodCongr g = let __src := f.prodCongr g.toEquiv; { toEquiv := __src, map_add' := }
Instances For
def MulEquiv.prodCongr {M : Type u_5} {N : Type u_6} [] [] {M' : Type u_8} {N' : Type u_9} [] [] (f : M ≃* M') (g : N ≃* N') :
M × N ≃* M' × N'

Product of multiplicative isomorphisms; the maps come from Equiv.prodCongr.

Equations
• f.prodCongr g = let __src := f.prodCongr g.toEquiv; { toEquiv := __src, map_mul' := }
Instances For
def AddEquiv.uniqueProd {M : Type u_5} {N : Type u_6} [] [] [] :
N × M ≃+ M

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

Equations
• AddEquiv.uniqueProd = let __src := ; { toEquiv := __src, map_add' := }
Instances For
theorem AddEquiv.uniqueProd.proof_1 {M : Type u_2} {N : Type u_1} [] [] [] :
∀ (x x_1 : N × M), ().toFun (x + x_1) = ().toFun (x + x_1)
def MulEquiv.uniqueProd {M : Type u_5} {N : Type u_6} [] [] [] :
N × M ≃* M

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

Equations
• MulEquiv.uniqueProd = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
theorem AddEquiv.prodUnique.proof_1 {M : Type u_1} {N : Type u_2} [] [] [] :
∀ (x x_1 : M × N), ().toFun (x + x_1) = ().toFun (x + x_1)
def AddEquiv.prodUnique {M : Type u_5} {N : Type u_6} [] [] [] :
M × N ≃+ M

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

Equations
• AddEquiv.prodUnique = let __src := ; { toEquiv := __src, map_add' := }
Instances For
def MulEquiv.prodUnique {M : Type u_5} {N : Type u_6} [] [] [] :
M × N ≃* M

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

Equations
• MulEquiv.prodUnique = let __src := ; { toEquiv := __src, map_mul' := }
Instances For
theorem AddEquiv.prodAddUnits.proof_5 {M : Type u_2} {N : Type u_1} [] [] (a : AddUnits (M × N)) (b : AddUnits (M × N)) :
(().prod ()) (a + b) = (().prod ()) a + (().prod ()) b
abbrev AddEquiv.prodAddUnits.match_1 {M : Type u_1} {N : Type u_2} [] [] (motive : Prop) :
∀ (x : ), (∀ (u₁ : ) (u₂ : ), motive (u₁, u₂))motive x
Equations
• =
Instances For
theorem AddEquiv.prodAddUnits.proof_4 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x : ), (().prod ()) ((fun (u : ) => { val := (u.1, u.2), neg := ((-u.1), (-u.2)), val_neg := , neg_val := }) x) = x
theorem AddEquiv.prodAddUnits.proof_1 {M : Type u_1} {N : Type u_2} [] [] (u : ) :
(u.1 + (-u.1), u.2 + (-u.2)) = 0
theorem AddEquiv.prodAddUnits.proof_2 {M : Type u_1} {N : Type u_2} [] [] (u : ) :
((-u.1) + u.1, (-u.2) + u.2) = 0
theorem AddEquiv.prodAddUnits.proof_3 {M : Type u_2} {N : Type u_1} [] [] (u : AddUnits (M × N)) :
{ val := (((().prod ()) u).1, ((().prod ()) u).2), neg := ((-((().prod ()) u).1), (-((().prod ()) u).2)), val_neg := , neg_val := } = u
def AddEquiv.prodAddUnits {M : Type u_5} {N : Type u_6} [] [] :

Equations
• One or more equations did not get rendered due to their size.
Instances For
def MulEquiv.prodUnits {M : Type u_5} {N : Type u_6} [] [] :
(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
• One or more equations did not get rendered due to their size.
Instances For
theorem AddUnits.embedProduct.proof_2 (α : Type u_1) [] (x : ) (y : ) :
def AddUnits.embedProduct (α : Type u_8) [] :

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

Equations
• = { toFun := fun (x : ) => (x, AddOpposite.op (-x)), map_zero' := , map_add' := }
Instances For
theorem AddUnits.embedProduct.proof_1 (α : Type u_1) [] :
@[simp]
theorem AddUnits.embedProduct_apply (α : Type u_8) [] (x : ) :
@[simp]
theorem Units.embedProduct_apply (α : Type u_8) [] (x : αˣ) :
x = (x, )
def Units.embedProduct (α : Type u_8) [] :

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

Equations
• = { toFun := fun (x : αˣ) => (x, ), map_one' := , map_mul' := }
Instances For

### Multiplication and division as homomorphisms #

∀ (x x_1 : α × α), x.1 + x_1.1 + (x.2 + x_1.2) = x.1 + x.2 + (x_1.1 + x_1.2)

Equations
• addAddHom = { toFun := fun (a : α × α) => a.1 + a.2, map_add' := }
Instances For
@[simp]
theorem mulMulHom_apply {α : Type u_8} [] (a : α × α) :
mulMulHom a = a.1 * a.2
@[simp]
theorem addAddHom_apply {α : Type u_8} [] (a : α × α) :
def mulMulHom {α : Type u_8} [] :
α × α →ₙ* α

Multiplication as a multiplicative homomorphism.

Equations
• mulMulHom = { toFun := fun (a : α × α) => a.1 * a.2, map_mul' := }
Instances For
α × α →+ α

Equations
Instances For
theorem addAddMonoidHom.proof_2 {α : Type u_1} [] (x : α × α) (y : α × α) :
0.1 + 0 = 0.1
@[simp]
theorem mulMonoidHom_apply {α : Type u_8} [] :
∀ (a : α × α), mulMonoidHom a = mulMulHom.toFun a
@[simp]
def mulMonoidHom {α : Type u_8} [] :
α × α →* α

Multiplication as a monoid homomorphism.

Equations
• mulMonoidHom = let __src := mulMulHom; { toFun := __src.toFun, map_one' := , map_mul' := }
Instances For
theorem subAddMonoidHom.proof_1 {α : Type u_1} :
0.1 - 0 = 0.1
theorem subAddMonoidHom.proof_2 {α : Type u_1} :
∀ (x x_1 : α × α), x.1 + x_1.1 - (x.2 + x_1.2) = x.1 - x.2 + (x_1.1 - x_1.2)
def subAddMonoidHom {α : Type u_8} :
α × α →+ α

Subtraction as an additive monoid homomorphism.

Equations
• subAddMonoidHom = { toFun := fun (a : α × α) => a.1 - a.2, map_zero' := , map_add' := }
Instances For
@[simp]
theorem divMonoidHom_apply {α : Type u_8} (a : α × α) :
divMonoidHom a = a.1 / a.2
@[simp]
theorem subAddMonoidHom_apply {α : Type u_8} (a : α × α) :
subAddMonoidHom a = a.1 - a.2
def divMonoidHom {α : Type u_8} :
α × α →* α

Division as a monoid homomorphism.

Equations
• divMonoidHom = { toFun := fun (a : α × α) => a.1 / a.2, map_one' := , map_mul' := }
Instances For