Documentation

Mathlib.Algebra.Group.Prod

Monoid, group etc structures on M × N #

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

Main declarations #

instance Prod.instMul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
Mul (M × N)
Equations
  • Prod.instMul = { mul := fun (p q : M × N) => (p.1 * q.1, p.2 * q.2) }
instance Prod.instAdd {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
Add (M × N)
Equations
  • Prod.instAdd = { add := fun (p q : M × N) => (p.1 + q.1, p.2 + q.2) }
@[simp]
theorem Prod.fst_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p q : M × N) :
(p * q).1 = p.1 * q.1
@[simp]
theorem Prod.fst_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p q : M × N) :
(p + q).1 = p.1 + q.1
@[simp]
theorem Prod.snd_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p q : M × N) :
(p * q).2 = p.2 * q.2
@[simp]
theorem Prod.snd_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p q : M × N) :
(p + q).2 = p.2 + q.2
@[simp]
theorem Prod.mk_mul_mk {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
@[simp]
theorem Prod.mk_add_mk {M : Type u_3} {N : Type u_4} [Add M] [Add N] (a₁ a₂ : M) (b₁ b₂ : N) :
(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
@[simp]
theorem Prod.swap_mul {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p q : M × N) :
(p * q).swap = p.swap * q.swap
@[simp]
theorem Prod.swap_add {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p q : M × N) :
(p + q).swap = p.swap + q.swap
theorem Prod.mul_def {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] (p q : M × N) :
p * q = (p.1 * q.1, p.2 * q.2)
theorem Prod.add_def {M : Type u_3} {N : Type u_4} [Add M] [Add N] (p q : M × N) :
p + q = (p.1 + q.1, p.2 + q.2)
theorem Prod.one_mk_mul_one_mk {M : Type u_3} {N : Type u_4} [Monoid 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} [AddMonoid 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] [Monoid 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] [AddMonoid N] (a₁ a₂ : M) :
(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
instance Prod.instOne {M : Type u_3} {N : Type u_4} [One M] [One N] :
One (M × N)
Equations
  • Prod.instOne = { one := (1, 1) }
instance Prod.instZero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
Zero (M × N)
Equations
  • Prod.instZero = { zero := (0, 0) }
@[simp]
theorem Prod.fst_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
1.1 = 1
@[simp]
theorem Prod.fst_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
0.1 = 0
@[simp]
theorem Prod.snd_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
1.2 = 1
@[simp]
theorem Prod.snd_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
0.2 = 0
theorem Prod.one_eq_mk {M : Type u_3} {N : Type u_4} [One M] [One N] :
1 = (1, 1)
theorem Prod.zero_eq_mk {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
0 = (0, 0)
@[simp]
theorem Prod.mk_one_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
(1, 1) = 1
@[simp]
theorem Prod.mk_zero_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
(0, 0) = 0
@[simp]
theorem Prod.mk_eq_one {M : Type u_3} {N : Type u_4} [One M] [One N] {x : M} {y : N} :
(x, y) = 1 x = 1 y = 1
@[simp]
theorem Prod.mk_eq_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] {x : M} {y : N} :
(x, y) = 0 x = 0 y = 0
@[simp]
theorem Prod.swap_one {M : Type u_3} {N : Type u_4} [One M] [One N] :
@[simp]
theorem Prod.swap_zero {M : Type u_3} {N : Type u_4} [Zero M] [Zero N] :
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.instInv {M : Type u_3} {N : Type u_4} [Inv M] [Inv N] :
Inv (M × N)
Equations
  • Prod.instInv = { inv := fun (p : M × N) => (p.1⁻¹, p.2⁻¹) }
instance Prod.instNeg {M : Type u_3} {N : Type u_4} [Neg M] [Neg N] :
Neg (M × N)
Equations
  • Prod.instNeg = { neg := fun (p : M × N) => (-p.1, -p.2) }
@[simp]
theorem Prod.fst_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :
p⁻¹.1 = p.1⁻¹
@[simp]
theorem Prod.fst_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :
(-p).1 = -p.1
@[simp]
theorem Prod.snd_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :
p⁻¹.2 = p.2⁻¹
@[simp]
theorem Prod.snd_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :
(-p).2 = -p.2
@[simp]
theorem Prod.inv_mk {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (a : G) (b : H) :
(a, b)⁻¹ = (a⁻¹, b⁻¹)
@[simp]
theorem Prod.neg_mk {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (a : G) (b : H) :
-(a, b) = (-a, -b)
@[simp]
theorem Prod.swap_inv {G : Type u_1} {H : Type u_2} [Inv G] [Inv H] (p : G × H) :
p⁻¹.swap = p.swap⁻¹
@[simp]
theorem Prod.swap_neg {G : Type u_1} {H : Type u_2} [Neg G] [Neg H] (p : G × H) :
(-p).swap = -p.swap
instance Prod.instInvolutiveInv {M : Type u_3} {N : Type u_4} [InvolutiveInv M] [InvolutiveInv N] :
Equations
instance Prod.instInvolutiveNeg {M : Type u_3} {N : Type u_4} [InvolutiveNeg M] [InvolutiveNeg N] :
Equations
instance Prod.instDiv {M : Type u_3} {N : Type u_4} [Div M] [Div N] :
Div (M × N)
Equations
  • Prod.instDiv = { div := fun (p q : M × N) => (p.1 / q.1, p.2 / q.2) }
instance Prod.instSub {M : Type u_3} {N : Type u_4} [Sub M] [Sub N] :
Sub (M × N)
Equations
  • Prod.instSub = { sub := fun (p q : M × N) => (p.1 - q.1, p.2 - q.2) }
@[simp]
theorem Prod.fst_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a b : G × H) :
(a / b).1 = a.1 / b.1
@[simp]
theorem Prod.fst_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a b : G × H) :
(a - b).1 = a.1 - b.1
@[simp]
theorem Prod.snd_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a b : G × H) :
(a / b).2 = a.2 / b.2
@[simp]
theorem Prod.snd_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a b : G × H) :
(a - b).2 = a.2 - b.2
@[simp]
theorem Prod.mk_div_mk {G : Type u_1} {H : Type u_2} [Div G] [Div H] (x₁ x₂ : G) (y₁ y₂ : H) :
(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
@[simp]
theorem Prod.mk_sub_mk {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (x₁ x₂ : G) (y₁ y₂ : H) :
(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
@[simp]
theorem Prod.swap_div {G : Type u_1} {H : Type u_2} [Div G] [Div H] (a b : G × H) :
(a / b).swap = a.swap / b.swap
@[simp]
theorem Prod.swap_sub {G : Type u_1} {H : Type u_2} [Sub G] [Sub H] (a b : G × H) :
(a - b).swap = a.swap - b.swap
theorem Prod.div_def {M : Type u_3} {N : Type u_4} [Div M] [Div N] (a b : M × N) :
a / b = (a.1 / b.1, a.2 / b.2)
theorem Prod.sub_def {M : Type u_3} {N : Type u_4} [Sub M] [Sub N] (a b : M × N) :
a - b = (a.1 - b.1, a.2 - b.2)
instance Prod.instSemigroup {M : Type u_3} {N : Type u_4} [Semigroup M] [Semigroup N] :
Equations
instance Prod.instAddSemigroup {M : Type u_3} {N : Type u_4} [AddSemigroup M] [AddSemigroup N] :
Equations
instance Prod.instCommSemigroup {G : Type u_1} {H : Type u_2} [CommSemigroup G] [CommSemigroup H] :
Equations
Equations
instance Prod.instMulOneClass {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
Equations
instance Prod.instAddZeroClass {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
Equations
instance Prod.instMonoid {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] :
Monoid (M × N)
Equations
instance Prod.instAddMonoid {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] :
Equations
instance Prod.instDivInvMonoid {G : Type u_1} {H : Type u_2} [DivInvMonoid G] [DivInvMonoid H] :
Equations
instance Prod.subNegMonoid {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] :
Equations
instance Prod.instDivisionMonoid {G : Type u_1} {H : Type u_2} [DivisionMonoid G] [DivisionMonoid H] :
Equations
Equations
Equations
Equations
instance Prod.instGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] :
Group (G × H)
Equations
instance Prod.instAddGroup {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] :
AddGroup (G × H)
Equations
theorem Prod.instIsCancelMul {G : Type u_1} {H : Type u_2} [Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] :
theorem Prod.instIsAddCancel {G : Type u_1} {H : Type u_2} [Add G] [Add H] [IsCancelAdd G] [IsCancelAdd H] :
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
instance Prod.instCancelMonoid {M : Type u_3} {N : Type u_4} [CancelMonoid M] [CancelMonoid N] :
Equations
Equations
instance Prod.instCommMonoid {M : Type u_3} {N : Type u_4} [CommMonoid M] [CommMonoid N] :
Equations
instance Prod.instAddCommMonoid {M : Type u_3} {N : Type u_4} [AddCommMonoid M] [AddCommMonoid N] :
Equations
Equations
Equations
instance Prod.instCommGroup {G : Type u_1} {H : Type u_2} [CommGroup G] [CommGroup H] :
Equations
instance Prod.instAddCommGroup {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] :
Equations
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) :
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) :
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) :
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) :
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.

Equations
  • MulHom.fst M N = { toFun := Prod.fst, map_mul' := }
Instances For
    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
      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
        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
          @[simp]
          theorem MulHom.coe_fst {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
          (MulHom.fst M N) = Prod.fst
          @[simp]
          theorem AddHom.coe_fst {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
          (AddHom.fst M N) = Prod.fst
          @[simp]
          theorem MulHom.coe_snd {M : Type u_3} {N : Type u_4} [Mul M] [Mul N] :
          (MulHom.snd M N) = Prod.snd
          @[simp]
          theorem AddHom.coe_snd {M : Type u_3} {N : Type u_4} [Add M] [Add N] :
          (AddHom.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).

          Equations
          • f.prod g = { toFun := Pi.prod f g, map_mul' := }
          Instances For
            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
              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) :
              (MulHom.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) :
              (AddHom.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) :
              (MulHom.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) :
              (AddHom.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) :
              ((MulHom.fst N P).comp f).prod ((MulHom.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) :
              ((AddHom.fst N P).comp f).prod ((AddHom.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.

              Equations
              Instances For
                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
                Instances For
                  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 (MulHom.fst M N)).prod (g.comp (MulHom.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 (AddHom.fst M N)).prod (g.comp (AddHom.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)

                  Equations
                  Instances For
                    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
                    Instances For
                      @[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.

                      Equations
                      • MonoidHom.fst M N = { toFun := Prod.fst, map_one' := , map_mul' := }
                      Instances For
                        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
                        Instances For
                          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
                            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
                            Instances For
                              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
                                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
                                  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
                                    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
                                      @[simp]
                                      theorem MonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      (MonoidHom.fst M N) = Prod.fst
                                      @[simp]
                                      theorem AddMonoidHom.coe_fst {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                      (AddMonoidHom.fst M N) = Prod.fst
                                      @[simp]
                                      theorem MonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      (MonoidHom.snd M N) = Prod.snd
                                      @[simp]
                                      theorem AddMonoidHom.coe_snd {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                      (AddMonoidHom.snd M N) = Prod.snd
                                      @[simp]
                                      theorem MonoidHom.inl_apply {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (x : M) :
                                      (MonoidHom.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) :
                                      (AddMonoidHom.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) :
                                      (MonoidHom.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) :
                                      (AddMonoidHom.inr M N) y = (0, y)
                                      @[simp]
                                      theorem MonoidHom.fst_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      @[simp]
                                      theorem MonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      (MonoidHom.snd M N).comp (MonoidHom.inl M N) = 1
                                      @[simp]
                                      theorem AddMonoidHom.snd_comp_inl {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                      @[simp]
                                      theorem MonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      (MonoidHom.fst M N).comp (MonoidHom.inr M N) = 1
                                      @[simp]
                                      theorem AddMonoidHom.fst_comp_inr {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                      @[simp]
                                      theorem MonoidHom.snd_comp_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                      theorem MonoidHom.commute_inl_inr {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] (m : M) (n : N) :
                                      Commute ((MonoidHom.inl M N) m) ((MonoidHom.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) :
                                      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
                                        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
                                          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) :
                                          (MonoidHom.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) :
                                          (AddMonoidHom.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) :
                                          (MonoidHom.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) :
                                          (AddMonoidHom.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) :
                                          ((MonoidHom.fst N P).comp f).prod ((MonoidHom.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) :
                                          ((AddMonoidHom.fst N P).comp f).prod ((AddMonoidHom.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.

                                          Equations
                                          Instances For
                                            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
                                            Instances For
                                              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 (MonoidHom.fst M N)).prod (g.comp (MonoidHom.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 (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.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.)

                                              Equations
                                              Instances For
                                                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
                                                Instances For
                                                  @[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 (MonoidHom.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 (AddMonoidHom.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 (MonoidHom.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 (AddMonoidHom.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 (MonoidHom.inl M N)).coprod (f.comp (MonoidHom.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 (AddMonoidHom.inl M N)).coprod (f.comp (AddMonoidHom.inr M N)) = f
                                                  @[simp]
                                                  theorem MonoidHom.coprod_inl_inr {M : Type u_6} {N : Type u_7} [CommMonoid M] [CommMonoid N] :
                                                  (MonoidHom.inl M N).coprod (MonoidHom.inr M N) = MonoidHom.id (M × N)
                                                  @[simp]
                                                  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.

                                                  Equations
                                                  Instances For
                                                    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
                                                    Instances For
                                                      @[simp]
                                                      theorem MulEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                                      MulEquiv.prodComm = Prod.swap
                                                      @[simp]
                                                      theorem AddEquiv.coe_prodComm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                                      AddEquiv.prodComm = Prod.swap
                                                      @[simp]
                                                      theorem MulEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [MulOneClass M] [MulOneClass N] :
                                                      MulEquiv.prodComm.symm = Prod.swap
                                                      @[simp]
                                                      theorem AddEquiv.coe_prodComm_symm {M : Type u_3} {N : Type u_4} [AddZeroClass M] [AddZeroClass N] :
                                                      AddEquiv.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.

                                                      Equations
                                                      Instances For
                                                        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
                                                        Instances For
                                                          @[simp]
                                                          theorem MulEquiv.coe_prodAssoc {M : Type u_3} {N : Type u_4} {P : Type u_5} [MulOneClass M] [MulOneClass N] [MulOneClass P] :
                                                          MulEquiv.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] :
                                                          AddEquiv.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] :
                                                          MulEquiv.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] :
                                                          AddEquiv.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.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            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
                                                              @[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') :
                                                              (AddEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)
                                                              @[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') :
                                                              (MulEquiv.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'] :
                                                              @[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'] :
                                                              @[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'] :
                                                              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
                                                                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
                                                                  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.

                                                                  Equations
                                                                  Instances For
                                                                    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.

                                                                    Equations
                                                                    Instances For
                                                                      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.

                                                                      Equations
                                                                      Instances For
                                                                        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.

                                                                        Equations
                                                                        Instances For
                                                                          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
                                                                            def AddEquiv.prodAddUnits {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid 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
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Units.embedProduct (α : Type u_6) [Monoid α] :

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

                                                                              Equations
                                                                              Instances For

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

                                                                                Equations
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Units.embedProduct_apply (α : Type u_6) [Monoid α] (x : αˣ) :
                                                                                  @[simp]
                                                                                  theorem AddUnits.embedProduct_apply (α : Type u_6) [AddMonoid α] (x : AddUnits α) :

                                                                                  Multiplication and division as homomorphisms #

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

                                                                                  Multiplication as a multiplicative homomorphism.

                                                                                  Equations
                                                                                  • mulMulHom = { toFun := fun (a : α × α) => a.1 * a.2, map_mul' := }
                                                                                  Instances For
                                                                                    def addAddHom {α : Type u_6} [AddCommSemigroup α] :
                                                                                    α × α →ₙ+ α

                                                                                    Addition as an additive homomorphism.

                                                                                    Equations
                                                                                    • addAddHom = { toFun := fun (a : α × α) => a.1 + a.2, map_add' := }
                                                                                    Instances For
                                                                                      @[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.

                                                                                      Equations
                                                                                      • mulMonoidHom = { toFun := mulMulHom.toFun, map_one' := , map_mul' := }
                                                                                      Instances For
                                                                                        def addAddMonoidHom {α : Type u_6} [AddCommMonoid α] :
                                                                                        α × α →+ α

                                                                                        Addition as an additive monoid homomorphism.

                                                                                        Equations
                                                                                        • addAddMonoidHom = { toFun := addAddHom.toFun, map_zero' := , map_add' := }
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem mulMonoidHom_apply {α : Type u_6} [CommMonoid α] (a✝ : α × α) :
                                                                                          mulMonoidHom a✝ = mulMulHom.toFun a✝
                                                                                          @[simp]
                                                                                          theorem addAddMonoidHom_apply {α : Type u_6} [AddCommMonoid α] (a✝ : α × α) :
                                                                                          addAddMonoidHom a✝ = addAddHom.toFun a✝
                                                                                          def divMonoidHom {α : Type u_6} [DivisionCommMonoid α] :
                                                                                          α × α →* α

                                                                                          Division as a monoid homomorphism.

                                                                                          Equations
                                                                                          • divMonoidHom = { toFun := fun (a : α × α) => a.1 / a.2, map_one' := , map_mul' := }
                                                                                          Instances For
                                                                                            def subAddMonoidHom {α : Type u_6} [SubtractionCommMonoid α] :
                                                                                            α × α →+ α

                                                                                            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_6} [DivisionCommMonoid α] (a : α × α) :
                                                                                              divMonoidHom a = a.1 / a.2
                                                                                              @[simp]
                                                                                              theorem subAddMonoidHom_apply {α : Type u_6} [SubtractionCommMonoid α] (a : α × α) :
                                                                                              subAddMonoidHom a = a.1 - a.2