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.

theorem Prod.one_mk_mul_one_mk {M : Type u_3} {N : Type u_4} [MulOneClass M] [Mul N] (b₁ b₂ : N) : (1, b₁) * (1, b₂) = (1, b₁ * b₂)

theorem Prod.zero_mk_add_zero_mk {M : Type u_3} {N : Type u_4} [AddZeroClass M] [Add N] (b₁ b₂ : N) : (0, b₁) + (0, b₂) = (0, b₁ + b₂)

theorem Prod.mk_one_mul_mk_one {M : Type u_3} {N : Type u_4} [Mul M] [MulOneClass N] (a₁ a₂ : M) : (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

theorem Prod.mk_zero_add_mk_zero {M : Type u_3} {N : Type u_4} [Add M] [AddZeroClass N] (a₁ a₂ : M) : (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)

theorem Prod.fst_mul_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (p : M × N) : (p.1, 1) * (1, p.2) = p

theorem Prod.fst_add_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (p : M × N) : (p.1, 0) + (0, p.2) = p

instance Prod.instInvolutiveInv {M : Type u_3} {N : Type u_4} [InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N)

instance Prod.instInvolutiveNeg {M : Type u_3} {N : Type u_4} [InvolutiveNeg M] [InvolutiveNeg N] : InvolutiveNeg (M × N)

instance Prod.instSemigroup {M : Type u_3} {N : Type u_4} [Semigroup M] [Semigroup N] : Semigroup (M × N)

instance Prod.instAddSemigroup {M : Type u_3} {N : Type u_4} [AddSemigroup M] [AddSemigroup N] : AddSemigroup (M × N)

instance Prod.instCommSemigroup {G : Type u_1} {H : Type u_2} [CommSemigroup G] [CommSemigroup H] : CommSemigroup (G × H)

instance Prod.instAddCommSemigroup {G : Type u_1} {H : Type u_2} [AddCommSemigroup G] [AddCommSemigroup H] : AddCommSemigroup (G × H)

instance Prod.instMulOneClass {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : MulOneClass (M × N)

instance Prod.instAddZeroClass {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : AddZeroClass (M × N)

instance Prod.instMonoid {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] : Monoid (M × N)

instance Prod.instAddMonoid {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] : AddMonoid (M × N)

instance Prod.instIsMulTorsionFree {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] [IsMulTorsionFree M] [IsMulTorsionFree N] : IsMulTorsionFree (M × N)

instance Prod.instDivInvMonoid {G : Type u_1} {H : Type u_2} [DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H)

instance Prod.subNegMonoid {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] : SubNegMonoid (G × H)

instance Prod.instDivisionMonoid {G : Type u_1} {H : Type u_2} [DivisionMonoid G] [DivisionMonoid H] : DivisionMonoid (G × H)

instance Prod.instSubtractionMonoid {G : Type u_1} {H : Type u_2} [SubtractionMonoid G] [SubtractionMonoid H] : SubtractionMonoid (G × H)

instance Prod.instDivisionCommMonoid {G : Type u_1} {H : Type u_2} [DivisionCommMonoid G] [DivisionCommMonoid H] : DivisionCommMonoid (G × H)

instance Prod.SubtractionCommMonoid {G : Type u_1} {H : Type u_2} [_root_.SubtractionCommMonoid G] [_root_.SubtractionCommMonoid H] : _root_.SubtractionCommMonoid (G × H)

instance Prod.instGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Group (G × H)

instance Prod.instAddGroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] : AddGroup (G × H)

instance Prod.instIsLeftCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] : IsLeftCancelMul (G × H)

instance Prod.instIsAddLeftCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsLeftCancelAdd G] [IsLeftCancelAdd H] : IsLeftCancelAdd (G × H)

instance Prod.instIsRightCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsRightCancelMul G] [IsRightCancelMul H] : IsRightCancelMul (G × H)

instance Prod.instIsAddRightCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsRightCancelAdd G] [IsRightCancelAdd H] : IsRightCancelAdd (G × H)

instance Prod.instIsCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] : IsCancelMul (G × H)

instance Prod.instIsAddCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsCancelAdd G] [IsCancelAdd H] : IsCancelAdd (G × H)

instance Prod.instLeftCancelSemigroup {G : Type u_1} {H : Type u_2} [LeftCancelSemigroup G] [LeftCancelSemigroup H] : LeftCancelSemigroup (G × H)

instance Prod.instAddLeftCancelSemigroup {G : Type u_1} {H : Type u_2} [AddLeftCancelSemigroup G] [AddLeftCancelSemigroup H] : AddLeftCancelSemigroup (G × H)

instance Prod.instRightCancelSemigroup {G : Type u_1} {H : Type u_2} [RightCancelSemigroup G] [RightCancelSemigroup H] : RightCancelSemigroup (G × H)

instance Prod.instAddRightCancelSemigroup {G : Type u_1} {H : Type u_2} [AddRightCancelSemigroup G] [AddRightCancelSemigroup H] : AddRightCancelSemigroup (G × H)

instance Prod.instLeftCancelMonoid {M : Type u_3} {N : Type u_4} [LeftCancelMonoid M] [LeftCancelMonoid N] : LeftCancelMonoid (M × N)

instance Prod.instAddLeftCancelMonoid {M : Type u_3} {N : Type u_4} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] : AddLeftCancelMonoid (M × N)

instance Prod.instRightCancelMonoid {M : Type u_3} {N : Type u_4} [RightCancelMonoid M] [RightCancelMonoid N] : RightCancelMonoid (M × N)

instance Prod.instAddRightCancelMonoid {M : Type u_3} {N : Type u_4} [AddRightCancelMonoid M] [AddRightCancelMonoid N] : AddRightCancelMonoid (M × N)

instance Prod.instCancelMonoid {M : Type u_3} {N : Type u_4} [CancelMonoid M] [CancelMonoid N] : CancelMonoid (M × N)

instance Prod.instAddCancelMonoid {M : Type u_3} {N : Type u_4} [AddCancelMonoid M] [AddCancelMonoid N] : AddCancelMonoid (M × N)

instance Prod.instCommMonoid {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] : CommMonoid (M × N)

instance Prod.instAddCommMonoid {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] : AddCommMonoid (M × N)

instance Prod.instCancelCommMonoid {M : Type u_3} {N : Type u_4} [CancelCommMonoid M] [CancelCommMonoid N] : CancelCommMonoid (M × N)

instance Prod.instAddCancelCommMonoid {M : Type u_3} {N : Type u_4} [AddCancelCommMonoid M] [AddCancelCommMonoid N] : AddCancelCommMonoid (M × N)

instance Prod.instCommGroup {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] : CommGroup (G × H)

instance Prod.instAddCommGroup {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] : AddCommGroup (G × H)

theorem SemiconjBy.prod {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x y z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z

theorem AddSemiconjBy.prod {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x y z : M × N} (hm : AddSemiconjBy x.1 y.1 z.1) (hn : AddSemiconjBy x.2 y.2 z.2) : AddSemiconjBy x y z

theorem Prod.semiconjBy_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x y z : M × N} : SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2

theorem Prod.addSemiconjBy_iff {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x y z : M × N} : AddSemiconjBy x y z ↔ AddSemiconjBy x.1 y.1 z.1 ∧ AddSemiconjBy x.2 y.2 z.2

theorem Commute.prod {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y

theorem AddCommute.prod {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x y : M × N} (hm : AddCommute x.1 y.1) (hn : AddCommute x.2 y.2) : AddCommute x y

theorem Prod.commute_iff {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] {x y : M × N} : Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2

theorem Prod.addCommute_iff {M : Type u_3} {N : Type u_4} [Add M] [Add N] {x y : M × N} : AddCommute x y ↔ AddCommute x.1 y.1 ∧ AddCommute x.2 y.2

def MulHom.fst (M : Type u_3) (N : Type u_4) [Mul M] [Mul N] : M × N →ₙ* M

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

def AddHom.fst (M : Type u_3) (N : Type u_4) [Add M] [Add N] : M × N →ₙ+ M

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

def MulHom.snd (M : Type u_3) (N : Type u_4) [Mul M] [Mul N] : M × N →ₙ* N

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

def AddHom.snd (M : Type u_3) (N : Type u_4) [Add M] [Add N] : M × N →ₙ+ N

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

@[simp]

theorem MulHom.coe_fst {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] : ⇑(fst M N) = Prod.fst

@[simp]

theorem AddHom.coe_fst {M : Type u_3} {N : Type u_4} [Add M] [Add N] : ⇑(fst M N) = Prod.fst

@[simp]

theorem MulHom.coe_snd {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] : ⇑(snd M N) = Prod.snd

@[simp]

theorem AddHom.coe_snd {M : Type u_3} {N : Type u_4} [Add M] [Add N] : ⇑(snd M N) = Prod.snd

def MulHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [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).

def AddHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : M →ₙ+ P) : M →ₙ+ N × P

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)

theorem MulHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod ⇑f ⇑g

theorem AddHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : M →ₙ+ P) : ⇑(f.prod g) = Pi.prod ⇑f ⇑g

@[simp]

theorem MulHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) : (f.prod g) x = (f x, g x)

@[simp]

theorem AddHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : M →ₙ+ P) (x : M) : (f.prod g) x = (f x, g x)

@[simp]

theorem MulHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : (fst N P).comp (f.prod g) = f

@[simp]

theorem AddHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : M →ₙ+ P) : (fst N P).comp (f.prod g) = f

@[simp]

theorem MulHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : (snd N P).comp (f.prod g) = g

@[simp]

theorem AddHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N) (g : M →ₙ+ P) : (snd N P).comp (f.prod g) = g

@[simp]

theorem MulHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

@[simp]

theorem AddHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [Add P] (f : M →ₙ+ N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

def MulHom.prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') : M × N →ₙ* M' × N'

Prod.map as a MonoidHom.

def AddHom.prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N') : M × N →ₙ+ M' × N'

Prod.map as an AddMonoidHom

theorem MulHom.prodMap_def {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') : f.prodMap g = (f.comp (fst M N)).prod (g.comp (snd M N))

theorem AddHom.prodMap_def {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N') : f.prodMap g = (f.comp (fst M N)).prod (g.comp (snd M N))

@[simp]

theorem MulHom.coe_prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

@[simp]

theorem AddHom.coe_prodMap {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] (f : M →ₙ+ M') (g : N →ₙ+ N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

theorem MulHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [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)

theorem AddHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} [Add M] [Add N] [Add M'] [Add N'] [Add 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 MulHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] (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)

def AddHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) : M × 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)

@[simp]

theorem MulHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) : (f.coprod g) p = f p.1 * g p.2

@[simp]

theorem AddHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] (f : M →ₙ+ P) (g : N →ₙ+ P) (p : M × N) : (f.coprod g) p = f p.1 + g p.2

theorem MulHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Mul M] [Mul N] [CommSemigroup P] {Q : Type u_6} [CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) : h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

theorem AddHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [Add M] [Add N] [AddCommSemigroup P] {Q : Type u_6} [AddCommSemigroup Q] (h : P →ₙ+ Q) (f : M →ₙ+ P) (g : N →ₙ+ P) : h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

def MonoidHom.fst (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] : M × N →* M

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

def AddMonoidHom.fst (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] : M × N →+ M

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

def MonoidHom.snd (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] : M × N →* N

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

def AddMonoidHom.snd (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] : M × N →+ N

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

def MonoidHom.inl (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] : M →* M × N

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

def AddMonoidHom.inl (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] : M →+ M × N

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

def MonoidHom.inr (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] : N →* M × N

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

def AddMonoidHom.inr (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] : N →+ M × N

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

@[simp]

theorem MonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : ⇑(fst M N) = Prod.fst

@[simp]

theorem AddMonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : ⇑(fst M N) = Prod.fst

@[simp]

theorem MonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : ⇑(snd M N) = Prod.snd

@[simp]

theorem AddMonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : ⇑(snd M N) = Prod.snd

@[simp]

theorem MonoidHom.inl_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (x : M) : (inl M N) x = (x, 1)

@[simp]

theorem AddMonoidHom.inl_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (x : M) : (inl M N) x = (x, 0)

@[simp]

theorem MonoidHom.inr_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (y : N) : (inr M N) y = (1, y)

@[simp]

theorem AddMonoidHom.inr_apply {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (y : N) : (inr M N) y = (0, y)

@[simp]

theorem MonoidHom.fst_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : (fst M N).comp (inl M N) = id M

@[simp]

theorem AddMonoidHom.fst_comp_inl {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : (fst M N).comp (inl M N) = id M

@[simp]

theorem MonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : (snd M N).comp (inl M N) = 1

@[simp]

theorem AddMonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : (snd M N).comp (inl M N) = 0

@[simp]

theorem MonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : (fst M N).comp (inr M N) = 1

@[simp]

theorem AddMonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : (fst M N).comp (inr M N) = 0

@[simp]

theorem MonoidHom.snd_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : (snd M N).comp (inr M N) = id N

@[simp]

theorem AddMonoidHom.snd_comp_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : (snd M N).comp (inr M N) = id N

theorem MonoidHom.commute_inl_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (m : M) (n : N) : Commute ((inl M N) m) ((inr M N) n)

theorem AddMonoidHom.addCommute_inl_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] (m : M) (n : N) : AddCommute ((inl M N) m) ((inr M N) n)

def MonoidHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass 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).

def AddMonoidHom.prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (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)

theorem MonoidHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Pi.prod ⇑f ⇑g

theorem AddMonoidHom.coe_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : ⇑(f.prod g) = Pi.prod ⇑f ⇑g

@[simp]

theorem MonoidHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) (x : M) : (f.prod g) x = (f x, g x)

@[simp]

theorem AddMonoidHom.prod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M) : (f.prod g) x = (f x, g x)

@[simp]

theorem MonoidHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : (fst N P).comp (f.prod g) = f

@[simp]

theorem AddMonoidHom.fst_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : (fst N P).comp (f.prod g) = f

@[simp]

theorem MonoidHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : (snd N P).comp (f.prod g) = g

@[simp]

theorem AddMonoidHom.snd_comp_prod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : (snd N P).comp (f.prod g) = g

@[simp]

theorem MonoidHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

@[simp]

theorem AddMonoidHom.prod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N × P) : ((fst N P).comp f).prod ((snd N P).comp f) = f

def MonoidHom.prodMap {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : M × N →* M' × N'

Prod.map as a MonoidHom.

def AddMonoidHom.prodMap {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : M × N →+ M' × N'

Prod.map as an AddMonoidHom.

theorem MonoidHom.prodMap_def {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : f.prodMap g = (f.comp (fst M N)).prod (g.comp (snd M N))

theorem AddMonoidHom.prodMap_def {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : f.prodMap g = (f.comp (fst M N)).prod (g.comp (snd M N))

@[simp]

theorem MonoidHom.coe_prodMap {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

@[simp]

theorem AddMonoidHom.coe_prodMap {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : ⇑(f.prodMap g) = Prod.map ⇑f ⇑g

theorem MonoidHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] [MulOneClass 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)

theorem AddMonoidHom.prod_comp_prodMap {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] [AddZeroClass 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 MonoidHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (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.)

def AddMonoidHom.coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (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.)

@[simp]

theorem MonoidHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) (p : M × N) : (f.coprod g) p = f p.1 * g p.2

@[simp]

theorem AddMonoidHom.coprod_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) (p : M × N) : (f.coprod g) p = f p.1 + g p.2

@[simp]

theorem MonoidHom.coprod_comp_inl {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) : (f.coprod g).comp (inl M N) = f

@[simp]

theorem AddMonoidHom.coprod_comp_inl {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) : (f.coprod g).comp (inl M N) = f

@[simp]

theorem MonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) : (f.coprod g).comp (inr M N) = g

@[simp]

theorem AddMonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) : (f.coprod g).comp (inr M N) = g

@[simp]

theorem MonoidHom.coprod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M × N →* P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f

@[simp]

theorem AddMonoidHom.coprod_unique {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M × N →+ P) : (f.comp (inl M N)).coprod (f.comp (inr M N)) = f

@[simp]

theorem MonoidHom.coprod_inl_inr {M : Type u_6} {N : Type u_7} [CommMonoid M] [CommMonoid N] : (inl M N).coprod (inr M N) = id (M × N)

@[simp]

theorem AddMonoidHom.coprod_inl_inr {M : Type u_6} {N : Type u_7} [AddCommMonoid M] [AddCommMonoid N] : (inl M N).coprod (inr M N) = id (M × N)

theorem MonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [CommMonoid P] {Q : Type u_6} [CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) : h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

theorem AddMonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] {Q : Type u_6} [AddCommMonoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P) : h.comp (f.coprod g) = (h.comp f).coprod (h.comp g)

def MulEquiv.prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : M × N ≃* N × M

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

def AddEquiv.prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : M × N ≃+ N × M

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

@[simp]

theorem MulEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : ⇑prodComm = Prod.swap

@[simp]

theorem AddEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : ⇑prodComm = Prod.swap

@[simp]

theorem MulEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] : ⇑prodComm.symm = Prod.swap

@[simp]

theorem AddEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] : ⇑prodComm.symm = Prod.swap

def MulEquiv.prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] : (M × N) × P ≃* M × N × P

The equivalence between (M × N) × P and M × (N × P) is multiplicative.

def AddEquiv.prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] : (M × N) × P ≃+ M × N × P

The equivalence between (M × N) × P and M × (N × P) is additive.

@[simp]

theorem MulEquiv.coe_prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] : ⇑prodAssoc = ⇑(Equiv.prodAssoc M N P)

@[simp]

theorem AddEquiv.coe_prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] : ⇑prodAssoc = ⇑(Equiv.prodAssoc M N P)

@[simp]

theorem MulEquiv.coe_prodAssoc_symm {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] : ⇑prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm

@[simp]

theorem AddEquiv.coe_prodAssoc_symm {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] : ⇑prodAssoc.symm = ⇑(Equiv.prodAssoc M N P).symm

def MulEquiv.prodProdProdComm (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] : (M × N) × M' × N' ≃* (M × M') × N × N'

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

def AddEquiv.prodProdProdComm (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] : (M × N) × M' × N' ≃+ (M × M') × N × N'

Four-way commutativity of Prod. The name matches mul_mul_mul_comm

@[simp]

theorem MulEquiv.prodProdProdComm_apply (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] (mnmn : (M × N) × M' × N') : (prodProdProdComm 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_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] (mnmn : (M × N) × M' × N') : (prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

@[simp]

theorem MulEquiv.prodProdProdComm_toEquiv (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] : ↑(prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

@[simp]

theorem AddEquiv.prodProdProdComm_toEquiv (M : Type u_3) (N : Type u_4) [AddZeroClass M] [AddZeroClass N] (M' : Type u_6) (N' : Type u_7) [AddZeroClass N'] [AddZeroClass M'] : ↑(prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

@[simp]

theorem MulEquiv.prodProdProdComm_symm (M : Type u_3) (N : Type u_4) [MulOneClass M] [MulOneClass N] (M' : Type u_6) (N' : Type u_7) [MulOneClass N'] [MulOneClass M'] : (prodProdProdComm M N M' N').symm = prodProdProdComm M M' N N'

def MulEquiv.prodCongr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass N'] [MulOneClass M'] (f : M ≃* M') (g : N ≃* N') : M × N ≃* M' × N'

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

def AddEquiv.prodCongr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass N'] [AddZeroClass M'] (f : M ≃+ M') (g : N ≃+ N') : M × N ≃+ M' × N'

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

def MulEquiv.uniqueProd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] [Unique N] : N × M ≃* M

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

This is the MulEquiv version of Equiv.uniqueProd.

def AddEquiv.uniqueProd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] [Unique N] : N × M ≃+ M

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

This is the AddEquiv version of Equiv.uniqueProd.

def MulEquiv.prodUnique {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] [Unique N] : M × N ≃* M

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

This is the MulEquiv version of Equiv.prodUnique.

def AddEquiv.prodUnique {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] [Unique N] : M × N ≃+ M

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

This is the AddEquiv version of Equiv.prodUnique.

def MulEquiv.prodUnits {M : Type u_3} {N : Type u_4} [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.

def AddEquiv.prodAddUnits {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] : AddUnits (M × N) ≃+ AddUnits M × AddUnits 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.

theorem Prod.isUnit_iff {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {x : M × N} : IsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2

theorem Prod.isAddUnit_iff {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] {x : M × N} : IsAddUnit x ↔ IsAddUnit x.1 ∧ IsAddUnit x.2

def Units.embedProduct (α : Type u_6) [Monoid α] : αˣ →* α × αᵐᵒᵖ

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

def AddUnits.embedProduct (α : Type u_6) [AddMonoid α] : AddUnits α →+ α × αᵃᵒᵖ

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

@[simp]

theorem Units.embedProduct_apply (α : Type u_6) [Monoid α] (x : αˣ) : (embedProduct α) x = (↑x, MulOpposite.op ↑x⁻¹)

@[simp]

theorem AddUnits.embedProduct_apply (α : Type u_6) [AddMonoid α] (x : AddUnits α) : (embedProduct α) x = (↑x, AddOpposite.op ↑(-x))

theorem Units.embedProduct_injective (α : Type u_6) [Monoid α] : Function.Injective ⇑(embedProduct α)

theorem AddUnits.embedProduct_injective (α : Type u_6) [AddMonoid α] : Function.Injective ⇑(embedProduct α)

Multiplication and division as homomorphisms

def mulMulHom {α : Type u_6} [CommSemigroup α] : α × α →ₙ* α

Multiplication as a multiplicative homomorphism.

def addAddHom {α : Type u_6} [AddCommSemigroup α] : α × α →ₙ+ α

Addition as an additive homomorphism.

@[simp]

theorem mulMulHom_apply {α : Type u_6} [CommSemigroup α] (a : α × α) : mulMulHom a = a.1 * a.2

@[simp]

theorem addAddHom_apply {α : Type u_6} [AddCommSemigroup α] (a : α × α) : addAddHom a = a.1 + a.2

def mulMonoidHom {α : Type u_6} [CommMonoid α] : α × α →* α

Multiplication as a monoid homomorphism.

def addAddMonoidHom {α : Type u_6} [AddCommMonoid α] : α × α →+ α

Addition as an additive monoid homomorphism.

@[simp]

theorem addAddMonoidHom_apply {α : Type u_6} [AddCommMonoid α] (a✝ : α × α) : addAddMonoidHom a✝ = addAddHom.toFun a✝

@[simp]

theorem mulMonoidHom_apply {α : Type u_6} [CommMonoid α] (a✝ : α × α) : mulMonoidHom a✝ = mulMulHom.toFun a✝

def divMonoidHom {α : Type u_6} [DivisionCommMonoid α] : α × α →* α

Division as a monoid homomorphism.

def subAddMonoidHom {α : Type u_6} [SubtractionCommMonoid α] : α × α →+ α

Subtraction as an additive monoid homomorphism.

@[simp]

theorem divMonoidHom_apply {α : Type u_6} [DivisionCommMonoid α] (a : α × α) : divMonoidHom a = a.1 / a.2

@[simp]

theorem subAddMonoidHom_apply {α : Type u_6} [SubtractionCommMonoid α] (a : α × α) : subAddMonoidHom a = a.1 - a.2