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.

source

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₂)

source

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₂)

source

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)

source

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)

source

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

source

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

source

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

InvolutiveInv (M × N)

Equations

Prod.instInvolutiveInv = { toInv := Prod.instInv, inv_inv := ⋯ }

source

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

InvolutiveNeg (M × N)

Equations

Prod.instInvolutiveNeg = { toNeg := Prod.instNeg, neg_neg := ⋯ }

source

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

Semigroup (M × N)

Equations

Prod.instSemigroup = { toMul := Prod.instMul, mul_assoc := ⋯ }

source

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

AddSemigroup (M × N)

Equations

Prod.instAddSemigroup = { toAdd := Prod.instAdd, add_assoc := ⋯ }

source

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

CommSemigroup (G × H)

Equations

Prod.instCommSemigroup = { toSemigroup := Prod.instSemigroup, mul_comm := ⋯ }

source

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

AddCommSemigroup (G × H)

Equations

Prod.instAddCommSemigroup = { toAddSemigroup := Prod.instAddSemigroup, add_comm := ⋯ }

source

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

MulOneClass (M × N)

Equations

Prod.instMulOneClass = { toOne := Prod.instOne, toMul := Prod.instMul, one_mul := ⋯, mul_one := ⋯ }

source

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

AddZeroClass (M × N)

Equations

Prod.instAddZeroClass = { toZero := Prod.instZero, toAdd := Prod.instAdd, zero_add := ⋯, add_zero := ⋯ }

source

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

Monoid (M × N)

Equations

One or more equations did not get rendered due to their size.

source

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

AddMonoid (M × N)

Equations

One or more equations did not get rendered due to their size.

source

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

IsMulTorsionFree (M × N)

source

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

DivInvMonoid (G × H)

Equations

One or more equations did not get rendered due to their size.

source

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

SubNegMonoid (G × H)

Equations

One or more equations did not get rendered due to their size.

source

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

DivisionMonoid (G × H)

Equations

Prod.instDivisionMonoid = { toDivInvMonoid := Prod.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }

source

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

SubtractionMonoid (G × H)

Equations

Prod.instSubtractionMonoid = { toSubNegMonoid := Prod.subNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }

source

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

DivisionCommMonoid (G × H)

Equations

Prod.instDivisionCommMonoid = { toDivisionMonoid := Prod.instDivisionMonoid, mul_comm := ⋯ }

source

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

_root_.SubtractionCommMonoid (G × H)

Equations

Prod.SubtractionCommMonoid = { toSubtractionMonoid := Prod.instSubtractionMonoid, add_comm := ⋯ }

source

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

Group (G × H)

Equations

Prod.instGroup = { toDivInvMonoid := Prod.instDivInvMonoid, inv_mul_cancel := ⋯ }

source

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

AddGroup (G × H)

Equations

Prod.instAddGroup = { toSubNegMonoid := Prod.subNegMonoid, neg_add_cancel := ⋯ }

source

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

IsLeftCancelMul (G × H)

source

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

IsLeftCancelAdd (G × H)

source

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

IsRightCancelMul (G × H)

source

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

IsRightCancelAdd (G × H)

source

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

IsCancelMul (G × H)

source

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

IsCancelAdd (G × H)

source

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

LeftCancelSemigroup (G × H)

Equations

Prod.instLeftCancelSemigroup = { toSemigroup := Prod.instSemigroup, mul_left_cancel := ⋯ }

source

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

AddLeftCancelSemigroup (G × H)

Equations

Prod.instAddLeftCancelSemigroup = { toAddSemigroup := Prod.instAddSemigroup, add_left_cancel := ⋯ }

source

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

RightCancelSemigroup (G × H)

Equations

Prod.instRightCancelSemigroup = { toSemigroup := Prod.instSemigroup, mul_right_cancel := ⋯ }

source

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

AddRightCancelSemigroup (G × H)

Equations

Prod.instAddRightCancelSemigroup = { toAddSemigroup := Prod.instAddSemigroup, add_right_cancel := ⋯ }

source

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

LeftCancelMonoid (M × N)

Equations

Prod.instLeftCancelMonoid = { toSemigroup := Prod.instSemigroup, toOne := Prod.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_left_cancel := ⋯ }

source

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

AddLeftCancelMonoid (M × N)

Equations

One or more equations did not get rendered due to their size.

source

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

RightCancelMonoid (M × N)

Equations

Prod.instRightCancelMonoid = { toSemigroup := Prod.instSemigroup, toOne := Prod.instOne, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯, mul_right_cancel := ⋯ }

source

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

AddRightCancelMonoid (M × N)

Equations

One or more equations did not get rendered due to their size.

source

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

CancelMonoid (M × N)

Equations

Prod.instCancelMonoid = { toLeftCancelMonoid := Prod.instLeftCancelMonoid, mul_right_cancel := ⋯ }

source

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

AddCancelMonoid (M × N)

Equations

Prod.instAddCancelMonoid = { toAddLeftCancelMonoid := Prod.instAddLeftCancelMonoid, add_right_cancel := ⋯ }

source

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

CommMonoid (M × N)

Equations

Prod.instCommMonoid = { toMonoid := Prod.instMonoid, mul_comm := ⋯ }

source

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

AddCommMonoid (M × N)

Equations

Prod.instAddCommMonoid = { toAddMonoid := Prod.instAddMonoid, add_comm := ⋯ }

source

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

CancelCommMonoid (M × N)

Equations

Prod.instCancelCommMonoid = { toCommMonoid := Prod.instCommMonoid, mul_left_cancel := ⋯ }

source

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

AddCancelCommMonoid (M × N)

Equations

Prod.instAddCancelCommMonoid = { toAddCommMonoid := Prod.instAddCommMonoid, add_left_cancel := ⋯ }

source

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

CommGroup (G × H)

Equations

Prod.instCommGroup = { toGroup := Prod.instGroup, mul_comm := ⋯ }

source

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

AddCommGroup (G × H)

Equations

Prod.instAddCommGroup = { toAddGroup := Prod.instAddGroup, add_comm := ⋯ }

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

MulHom.fst M N = { toFun := Prod.fst, map_mul' := ⋯ }

Instances For

source

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

Equations

AddHom.fst M N = { toFun := Prod.fst, map_add' := ⋯ }

Instances For

source

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.

Equations

MulHom.snd M N = { toFun := Prod.snd, map_mul' := ⋯ }

Instances For

source

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

Equations

AddHom.snd M N = { toFun := Prod.snd, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MulHom.coe_fst {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

⇑(fst M N) = Prod.fst

source

@[simp]

theorem AddHom.coe_fst {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

⇑(fst M N) = Prod.fst

source

@[simp]

theorem MulHom.coe_snd {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :

⇑(snd M N) = Prod.snd

source

@[simp]

theorem AddHom.coe_snd {M : Type u_3} {N : Type u_4} [Add M] [Add N] :

⇑(snd M N) = Prod.snd

source

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).

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_mul' := ⋯ }

Instances For

source

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)

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_add' := ⋯ }

Instances For

source

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

source

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

source

@[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)

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))

Instances For

source

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

Equations

f.prodMap g = (f.comp (AddHom.fst M N)).prod (g.comp (AddHom.snd M N))

Instances For

source

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))

source

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))

source

@[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

source

@[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

source

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)

source

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)

source

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)

Equations

f.coprod g = f.comp (MulHom.fst M N) * g.comp (MulHom.snd M N)

Instances For

source

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)

Equations

f.coprod g = f.comp (AddHom.fst M N) + g.comp (AddHom.snd M N)

Instances For

source

@[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

source

@[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

source

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)

source

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)

source

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.

Equations

MonoidHom.fst M N = { toFun := Prod.fst, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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

Equations

AddMonoidHom.fst M N = { toFun := Prod.fst, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

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.

Equations

MonoidHom.snd M N = { toFun := Prod.snd, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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

Equations

AddMonoidHom.snd M N = { toFun := Prod.snd, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

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.

Equations

MonoidHom.inl M N = { toFun := fun (x : M) => (x, 1), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddMonoidHom.inl M N = { toFun := fun (x : M) => (x, 0), map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

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.

Equations

MonoidHom.inr M N = { toFun := fun (y : N) => (1, y), map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddMonoidHom.inr M N = { toFun := fun (y : N) => (0, y), map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑(fst M N) = Prod.fst

source

@[simp]

theorem AddMonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑(fst M N) = Prod.fst

source

@[simp]

theorem MonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑(snd M N) = Prod.snd

source

@[simp]

theorem AddMonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑(snd M N) = Prod.snd

source

@[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)

source

@[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)

source

@[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)

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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)

source

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)

source

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).

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

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)

Equations

f.prod g = { toFun := Pi.prod ⇑f ⇑g, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

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

source

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

source

@[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)

source

@[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)

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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.

Equations

f.prodMap g = (f.comp (MonoidHom.fst M N)).prod (g.comp (MonoidHom.snd M N))

Instances For

source

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.

Equations

f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))

Instances For

source

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))

source

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))

source

@[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

source

@[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

source

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)

source

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)

source

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.)

Equations

f.coprod g = f.comp (MonoidHom.fst M N) * g.comp (MonoidHom.snd M N)

Instances For

source

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.)

Equations

f.coprod g = f.comp (AddMonoidHom.fst M N) + g.comp (AddMonoidHom.snd M N)

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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)

source

@[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)

source

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)

source

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)

source

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.

Equations

MulEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddEquiv.prodComm = { toEquiv := Equiv.prodComm M N, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MulEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑prodComm = Prod.swap

source

@[simp]

theorem AddEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑prodComm = Prod.swap

source

@[simp]

theorem MulEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :

⇑prodComm.symm = Prod.swap

source

@[simp]

theorem AddEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :

⇑prodComm.symm = Prod.swap

source

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.

Equations

MulEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddEquiv.prodAssoc = { toEquiv := Equiv.prodAssoc M N P, map_add' := ⋯ }

Instances For

source

@[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)

source

@[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)

source

@[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

source

@[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

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[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)

source

@[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)

source

@[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'

source

@[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'

source

@[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'

source

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.

Equations

f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_mul' := ⋯ }

Instances For

source

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.

Equations

f.prodCongr g = { toEquiv := f.prodCongr g.toEquiv, map_add' := ⋯ }

Instances For

source

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.

Equations

MulEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_add' := ⋯ }

Instances For

source

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.

Equations

MulEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_mul' := ⋯ }

Instances For

source

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.

Equations

AddEquiv.prodUnique = { toEquiv := Equiv.prodUnique M N, map_add' := ⋯ }

Instances For

source

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.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

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.

Equations