Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon, Patrick Massot, Yury Kudryashov

! This file was ported from Lean 3 source module algebra.group.prod
! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Opposite
import Mathlib.Algebra.GroupWithZero.Units.Basic
import Mathlib.Algebra.Hom.Units

/-!
# 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 `MonoidHom`s:

* `fst M N : M × N →* M`, `snd M N : M × N →* N`: projections `Prod.fst` and `Prod.snd`
  as `MonoidHom`s;
* `inl M N : M →* M × N`, `inr M N : N →* M × N`: inclusions of first/second monoid
  into the product;
* `f.prod g : `M →* N × P`: sends `x` to `(f x, g x)`;
* `f.coprod g : M × N →* P`: sends `(x, y)` to `f x * g y`;
* `f.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`/`mulMonoidWithZeroHom`: Multiplication bundled as a
  multiplicative/monoid/monoid with zero homomorphism.
* `divMonoidHom`/`divMonoidWithZeroHom`: Division bundled as a monoid/monoid with zero
  homomorphism.
-/


variable {
A: Type ?u.23
A
:
Type _: Type (?u.59943+1)
Type _
} {
B: Type ?u.26
B
:
Type _: Type (?u.21364+1)
Type _
} {
G: Type ?u.39690
G
:
Type _: Type (?u.15455+1)
Type _
} {
H: Type ?u.32
H
:
Type _: Type (?u.1002+1)
Type _
} {
M: Type ?u.14
M
:
Type _: Type (?u.1005+1)
Type _
} {
N: Type ?u.39699
N
:
Type _: Type (?u.7978+1)
Type _
} {
P: Type ?u.39702
P
:
Type _: Type (?u.42267+1)
Type _
} namespace Prod @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst : Add N] → Add (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Mul M] → [inst : Mul N] → Mul (M × N)
instance
[
Mul: Type ?u.44 → Type ?u.44
Mul
M: Type ?u.35
M
] [
Mul: Type ?u.47 → Type ?u.47
Mul
N: Type ?u.38
N
] :
Mul: Type ?u.50 → Type ?u.50
Mul
(
M: Type ?u.35
M
×
N: Type ?u.38
N
) := ⟨fun
p: ?m.62
p
q: ?m.65
q
=> ⟨
p: ?m.62
p
.
1: {α : Type ?u.81} → {β : Type ?u.80} → α × β → α
1
*
q: ?m.65
q
.
1: {α : Type ?u.85} → {β : Type ?u.84} → α × β → α
1
,
p: ?m.62
p
.
2: {α : Type ?u.129} → {β : Type ?u.128} → α × β → β
2
*
q: ?m.65
q
.
2: {α : Type ?u.133} → {β : Type ?u.132} → α × β → β
2
⟩⟩ @[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).fst = p.fst + q.fst
to_additive
(attr := simp)] theorem
fst_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).fst = p.fst * q.fst
fst_mul
[
Mul: Type ?u.526 → Type ?u.526
Mul
M: Type ?u.517
M
] [
Mul: Type ?u.529 → Type ?u.529
Mul
N: Type ?u.520
N
] (
p: M × N
p
q: M × N
q
:
M: Type ?u.517
M
×
N: Type ?u.520
N
) : (
p: M × N
p
*
q: M × N
q
).
1: {α : Type ?u.615} → {β : Type ?u.614} → α × β → α
1
=
p: M × N
p
.
1: {α : Type ?u.624} → {β : Type ?u.623} → α × β → α
1
*
q: M × N
q
.
1: {α : Type ?u.628} → {β : Type ?u.627} → α × β → α
1
:=
rfl: ∀ {α : Sort ?u.672} {a : α}, a = a
rfl
#align prod.fst_mul
Prod.fst_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).fst = p.fst * q.fst
Prod.fst_mul
#align prod.fst_add
Prod.fst_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).fst = p.fst + q.fst
Prod.fst_add
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).snd = p.snd + q.snd
to_additive
(attr := simp)] theorem
snd_mul: ∀ [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).snd = p.snd * q.snd
snd_mul
[
Mul: Type ?u.770 → Type ?u.770
Mul
M: Type ?u.761
M
] [
Mul: Type ?u.773 → Type ?u.773
Mul
N: Type ?u.764
N
] (
p: M × N
p
q: M × N
q
:
M: Type ?u.761
M
×
N: Type ?u.764
N
) : (
p: M × N
p
*
q: M × N
q
).
2: {α : Type ?u.859} → {β : Type ?u.858} → α × β → β
2
=
p: M × N
p
.
2: {α : Type ?u.868} → {β : Type ?u.867} → α × β → β
2
*
q: M × N
q
.
2: {α : Type ?u.872} → {β : Type ?u.871} → α × β → β
2
:=
rfl: ∀ {α : Sort ?u.916} {a : α}, a = a
rfl
#align prod.snd_mul
Prod.snd_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), (p * q).snd = p.snd * q.snd
Prod.snd_mul
#align prod.snd_add
Prod.snd_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), (p + q).snd = p.snd + q.snd
Prod.snd_add
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N), (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
to_additive
(attr := simp)] theorem
mk_mul_mk: ∀ [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N), (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
mk_mul_mk
[
Mul: Type ?u.1014 → Type ?u.1014
Mul
M: Type ?u.1005
M
] [
Mul: Type ?u.1017 → Type ?u.1017
Mul
N: Type ?u.1008
N
] (
a₁: M
a₁
a₂: M
a₂
:
M: Type ?u.1005
M
) (
b₁: N
b₁
b₂: N
b₂
:
N: Type ?u.1008
N
) : (
a₁: M
a₁
,
b₁: N
b₁
) * (
a₂: M
a₂
,
b₂: N
b₂
) = (
a₁: M
a₁
*
a₂: M
a₂
,
b₁: N
b₁
*
b₂: N
b₂
) :=
rfl: ∀ {α : Sort ?u.1200} {a : α}, a = a
rfl
#align prod.mk_mul_mk
Prod.mk_mul_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (a₁ a₂ : M) (b₁ b₂ : N), (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂)
Prod.mk_mul_mk
#align prod.mk_add_mk
Prod.mk_add_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (a₁ a₂ : M) (b₁ b₂ : N), (a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)
Prod.mk_add_mk
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), swap (p + q) = swap p + swap q
to_additive
(attr := simp)] theorem
swap_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), swap (p * q) = swap p * swap q
swap_mul
[
Mul: Type ?u.1332 → Type ?u.1332
Mul
M: Type ?u.1323
M
] [
Mul: Type ?u.1335 → Type ?u.1335
Mul
N: Type ?u.1326
N
] (
p: M × N
p
q: M × N
q
:
M: Type ?u.1323
M
×
N: Type ?u.1326
N
) : (
p: M × N
p
*
q: M × N
q
).
swap: {α : Type ?u.1421} → {β : Type ?u.1420} → α × β → β × α
swap
=
p: M × N
p
.
swap: {α : Type ?u.1433} → {β : Type ?u.1432} → α × β → β × α
swap
*
q: M × N
q
.
swap: {α : Type ?u.1440} → {β : Type ?u.1439} → α × β → β × α
swap
:=
rfl: ∀ {α : Sort ?u.1507} {a : α}, a = a
rfl
#align prod.swap_mul
Prod.swap_mul: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), swap (p * q) = swap p * swap q
Prod.swap_mul
#align prod.swap_add
Prod.swap_add: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), swap (p + q) = swap p + swap q
Prod.swap_add
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), p + q = (p.fst + q.fst, p.snd + q.snd)
to_additive
] theorem
mul_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), p * q = (p.fst * q.fst, p.snd * q.snd)
mul_def
[
Mul: Type ?u.1619 → Type ?u.1619
Mul
M: Type ?u.1610
M
] [
Mul: Type ?u.1622 → Type ?u.1622
Mul
N: Type ?u.1613
N
] (
p: M × N
p
q: M × N
q
:
M: Type ?u.1610
M
×
N: Type ?u.1613
N
) :
p: M × N
p
*
q: M × N
q
= (
p: M × N
p
.
1: {α : Type ?u.1645} → {β : Type ?u.1644} → α × β → α
1
*
q: M × N
q
.
1: {α : Type ?u.1651} → {β : Type ?u.1650} → α × β → α
1
,
p: M × N
p
.
2: {α : Type ?u.1696} → {β : Type ?u.1695} → α × β → β
2
*
q: M × N
q
.
2: {α : Type ?u.1700} → {β : Type ?u.1699} → α × β → β
2
) :=
rfl: ∀ {α : Sort ?u.1811} {a : α}, a = a
rfl
#align prod.mul_def
Prod.mul_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (p q : M × N), p * q = (p.fst * q.fst, p.snd * q.snd)
Prod.mul_def
#align prod.add_def
Prod.add_def: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (p q : M × N), p + q = (p.fst + q.fst, p.snd + q.snd)
Prod.add_def
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : Add N] (b₁ b₂ : N), (0, b₁) + (0, b₂) = (0, b₁ + b₂)
to_additive
] theorem
one_mk_mul_one_mk: ∀ [inst : Monoid M] [inst_1 : Mul N] (b₁ b₂ : N), (1, b₁) * (1, b₂) = (1, b₁ * b₂)
one_mk_mul_one_mk
[
Monoid: Type ?u.1869 → Type ?u.1869
Monoid
M: Type ?u.1860
M
] [
Mul: Type ?u.1872 → Type ?u.1872
Mul
N: Type ?u.1863
N
] (
b₁: N
b₁
b₂: N
b₂
:
N: Type ?u.1863
N
) : ((
1: ?m.1889
1
:
M: Type ?u.1860
M
),
b₁: N
b₁
) * (
1: ?m.2018
1
,
b₂: N
b₂
) = (
1: ?m.2037
1
,
b₁: N
b₁
*
b₂: N
b₂
) :=

Goals accomplished! 🐙
A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N


(1, b₁) * (1, b₂) = (1, b₁ * b₂)
A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N


(1, b₁) * (1, b₂) = (1, b₁ * b₂)
A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N


(1 * 1, b₁ * b₂) = (1, b₁ * b₂)
A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N


(1, b₁) * (1, b₂) = (1, b₁ * b₂)
A: Type ?u.1848

B: Type ?u.1851

G: Type ?u.1854

H: Type ?u.1857

M: Type u_1

N: Type u_2

P: Type ?u.1866

inst✝¹: Monoid M

inst✝: Mul N

b₁, b₂: N


(1, b₁ * b₂) = (1, b₁ * b₂)

Goals accomplished! 🐙
#align prod.one_mk_mul_one_mk
Prod.one_mk_mul_one_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Mul N] (b₁ b₂ : N), (1, b₁) * (1, b₂) = (1, b₁ * b₂)
Prod.one_mk_mul_one_mk
#align prod.zero_mk_add_zero_mk
Prod.zero_mk_add_zero_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : Add N] (b₁ b₂ : N), (0, b₁) + (0, b₂) = (0, b₁ + b₂)
Prod.zero_mk_add_zero_mk
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : AddMonoid N] (a₁ a₂ : M), (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
to_additive
] theorem
mk_one_mul_mk_one: ∀ [inst : Mul M] [inst_1 : Monoid N] (a₁ a₂ : M), (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
mk_one_mul_mk_one
[
Mul: Type ?u.2655 → Type ?u.2655
Mul
M: Type ?u.2646
M
] [
Monoid: Type ?u.2658 → Type ?u.2658
Monoid
N: Type ?u.2649
N
] (
a₁: M
a₁
a₂: M
a₂
:
M: Type ?u.2646
M
) : (
a₁: M
a₁
, (
1: ?m.2675
1
:
N: Type ?u.2649
N
)) * (
a₂: M
a₂
,
1: ?m.2804
1
) = (
a₁: M
a₁
*
a₂: M
a₂
,
1: ?m.2869
1
) :=

Goals accomplished! 🐙
A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M


(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M


(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M


(a₁ * a₂, 1 * 1) = (a₁ * a₂, 1)
A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M


(a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
A: Type ?u.2634

B: Type ?u.2637

G: Type ?u.2640

H: Type ?u.2643

M: Type u_1

N: Type u_2

P: Type ?u.2652

inst✝¹: Mul M

inst✝: Monoid N

a₁, a₂: M


(a₁ * a₂, 1) = (a₁ * a₂, 1)

Goals accomplished! 🐙
#align prod.mk_one_mul_mk_one
Prod.mk_one_mul_mk_one: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Monoid N] (a₁ a₂ : M), (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)
Prod.mk_one_mul_mk_one
#align prod.mk_zero_add_mk_zero
Prod.mk_zero_add_mk_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : AddMonoid N] (a₁ a₂ : M), (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)
Prod.mk_zero_add_mk_zero
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Zero M] → [inst : Zero N] → Zero (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : One M] → [inst : One N] → One (M × N)
instance
[
One: Type ?u.3442 → Type ?u.3442
One
M: Type ?u.3433
M
] [
One: Type ?u.3445 → Type ?u.3445
One
N: Type ?u.3436
N
] :
One: Type ?u.3448 → Type ?u.3448
One
(
M: Type ?u.3433
M
×
N: Type ?u.3436
N
) := ⟨(
1: ?m.3466
1
,
1: ?m.3488
1
)⟩ @[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.fst = 0
to_additive
(attr := simp)] theorem
fst_one: ∀ [inst : One M] [inst_1 : One N], 1.fst = 1
fst_one
[
One: Type ?u.3681 → Type ?u.3681
One
M: Type ?u.3672
M
] [
One: Type ?u.3684 → Type ?u.3684
One
N: Type ?u.3675
N
] : (
1: ?m.3692
1
:
M: Type ?u.3672
M
×
N: Type ?u.3675
N
).
1: {α : Type ?u.3747} → {β : Type ?u.3746} → α × β → α
1
=
1: ?m.3751
1
:=
rfl: ∀ {α : Sort ?u.3787} {a : α}, a = a
rfl
#align prod.fst_one
Prod.fst_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.fst = 1
Prod.fst_one
#align prod.fst_zero
Prod.fst_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.fst = 0
Prod.fst_zero
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.snd = 0
to_additive
(attr := simp)] theorem
snd_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.snd = 1
snd_one
[
One: Type ?u.3861 → Type ?u.3861
One
M: Type ?u.3852
M
] [
One: Type ?u.3864 → Type ?u.3864
One
N: Type ?u.3855
N
] : (
1: ?m.3872
1
:
M: Type ?u.3852
M
×
N: Type ?u.3855
N
).
2: {α : Type ?u.3927} → {β : Type ?u.3926} → α × β → β
2
=
1: ?m.3931
1
:=
rfl: ∀ {α : Sort ?u.3967} {a : α}, a = a
rfl
#align prod.snd_one
Prod.snd_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1.snd = 1
Prod.snd_one
#align prod.snd_zero
Prod.snd_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0.snd = 0
Prod.snd_zero
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0 = (0, 0)
to_additive
] theorem
one_eq_mk: ∀ [inst : One M] [inst_1 : One N], 1 = (1, 1)
one_eq_mk
[
One: Type ?u.4041 → Type ?u.4041
One
M: Type ?u.4032
M
] [
One: Type ?u.4044 → Type ?u.4044
One
N: Type ?u.4035
N
] : (
1: ?m.4052
1
:
M: Type ?u.4032
M
×
N: Type ?u.4035
N
) = (
1: ?m.4111
1
,
1: ?m.4121
1
) :=
rfl: ∀ {α : Sort ?u.4206} {a : α}, a = a
rfl
#align prod.one_eq_mk
Prod.one_eq_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], 1 = (1, 1)
Prod.one_eq_mk
#align prod.zero_eq_mk
Prod.zero_eq_mk: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], 0 = (0, 0)
Prod.zero_eq_mk
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, (x, y) = 0 ↔ x = 0 ∧ y = 0
to_additive
(attr := simp)] theorem
mk_eq_one: ∀ [inst : One M] [inst_1 : One N] {x : M} {y : N}, (x, y) = 1 ↔ x = 1 ∧ y = 1
mk_eq_one
[
One: Type ?u.4254 → Type ?u.4254
One
M: Type ?u.4245
M
] [
One: Type ?u.4257 → Type ?u.4257
One
N: Type ?u.4248
N
] {
x: M
x
:
M: Type ?u.4245
M
} {
y: N
y
:
N: Type ?u.4248
N
} : (
x: M
x
,
y: N
y
) =
1: ?m.4270
1
↔
x: M
x
=
1: ?m.4338
1
∧
y: N
y
=
1: ?m.4373
1
:=
mk.inj_iff: ∀ {α : Type ?u.4411} {β : Type ?u.4412} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
#align prod.mk_eq_one
Prod.mk_eq_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] {x : M} {y : N}, (x, y) = 1 ↔ x = 1 ∧ y = 1
Prod.mk_eq_one
#align prod.mk_eq_zero
Prod.mk_eq_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] {x : M} {y : N}, (x, y) = 0 ↔ x = 0 ∧ y = 0
Prod.mk_eq_zero
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], swap 0 = 0
to_additive
(attr := simp)] theorem
swap_one: ∀ [inst : One M] [inst_1 : One N], swap 1 = 1
swap_one
[
One: Type ?u.4552 → Type ?u.4552
One
M: Type ?u.4543
M
] [
One: Type ?u.4555 → Type ?u.4555
One
N: Type ?u.4546
N
] : (
1: ?m.4563
1
:
M: Type ?u.4543
M
×
N: Type ?u.4546
N
).
swap: {α : Type ?u.4618} → {β : Type ?u.4617} → α × β → β × α
swap
=
1: ?m.4625
1
:=
rfl: ∀ {α : Sort ?u.4681} {a : α}, a = a
rfl
#align prod.swap_one
Prod.swap_one: ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N], swap 1 = 1
Prod.swap_one
#align prod.swap_zero
Prod.swap_zero: ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N], swap 0 = 0
Prod.swap_zero
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (p : M × N), (p.fst, 0) + (0, p.snd) = p
to_additive
] theorem
fst_mul_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N), (p.fst, 1) * (1, p.snd) = p
fst_mul_snd
[
MulOneClass: Type ?u.4765 → Type ?u.4765
MulOneClass
M: Type ?u.4756
M
] [
MulOneClass: Type ?u.4768 → Type ?u.4768
MulOneClass
N: Type ?u.4759
N
] (
p: M × N
p
:
M: Type ?u.4756
M
×
N: Type ?u.4759
N
) : (
p: M × N
p
.
fst: {α : Type ?u.4784} → {β : Type ?u.4783} → α × β → α
fst
,
1: ?m.4790
1
) * (
1: ?m.4804
1
,
p: M × N
p
.
snd: {α : Type ?u.4814} → {β : Type ?u.4813} → α × β → β
snd
) =
p: M × N
p
:=
ext: ∀ {α : Type ?u.5462} {β : Type ?u.5463} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
mul_one: ∀ {M : Type ?u.5473} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
p: M × N
p
.
1: {α : Type ?u.5477} → {β : Type ?u.5476} → α × β → α
1
) (
one_mul: ∀ {M : Type ?u.5492} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul
p: M × N
p
.
2: {α : Type ?u.5496} → {β : Type ?u.5495} → α × β → β
2
) #align prod.fst_mul_snd
Prod.fst_mul_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N), (p.fst, 1) * (1, p.snd) = p
Prod.fst_mul_snd
#align prod.fst_add_snd
Prod.fst_add_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (p : M × N), (p.fst, 0) + (0, p.snd) = p
Prod.fst_add_snd
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Neg M] → [inst : Neg N] → Neg (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Inv M] → [inst : Inv N] → Inv (M × N)
instance
[
Inv: Type ?u.5558 → Type ?u.5558
Inv
M: Type ?u.5549
M
] [
Inv: Type ?u.5561 → Type ?u.5561
Inv
N: Type ?u.5552
N
] :
Inv: Type ?u.5564 → Type ?u.5564
Inv
(
M: Type ?u.5549
M
×
N: Type ?u.5552
N
) := ⟨fun
p: ?m.5576
p
=> (
p: ?m.5576
p
.
1: {α : Type ?u.5604} → {β : Type ?u.5603} → α × β → α
1
⁻¹,
p: ?m.5576
p
.
2: {α : Type ?u.5635} → {β : Type ?u.5634} → α × β → β
2
⁻¹)⟩ @[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).fst = -p.fst
to_additive
(attr := simp)] theorem
fst_inv: ∀ [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.fst = p.fst⁻¹
fst_inv
[
Inv: Type ?u.5889 → Type ?u.5889
Inv
G: Type ?u.5874
G
] [
Inv: Type ?u.5892 → Type ?u.5892
Inv
H: Type ?u.5877
H
] (
p: G × H
p
:
G: Type ?u.5874
G
×
H: Type ?u.5877
H
) :
p: G × H
p
⁻¹.
1: {α : Type ?u.5938} → {β : Type ?u.5937} → α × β → α
1
=
p: G × H
p
.
1: {α : Type ?u.5945} → {β : Type ?u.5944} → α × β → α
1
⁻¹ :=
rfl: ∀ {α : Sort ?u.5959} {a : α}, a = a
rfl
#align prod.fst_inv
Prod.fst_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.fst = p.fst⁻¹
Prod.fst_inv
#align prod.fst_neg
Prod.fst_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).fst = -p.fst
Prod.fst_neg
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).snd = -p.snd
to_additive
(attr := simp)] theorem
snd_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.snd = p.snd⁻¹
snd_inv
[
Inv: Type ?u.6042 → Type ?u.6042
Inv
G: Type ?u.6027
G
] [
Inv: Type ?u.6045 → Type ?u.6045
Inv
H: Type ?u.6030
H
] (
p: G × H
p
:
G: Type ?u.6027
G
×
H: Type ?u.6030
H
) :
p: G × H
p
⁻¹.
2: {α : Type ?u.6091} → {β : Type ?u.6090} → α × β → β
2
=
p: G × H
p
.
2: {α : Type ?u.6098} → {β : Type ?u.6097} → α × β → β
2
⁻¹ :=
rfl: ∀ {α : Sort ?u.6112} {a : α}, a = a
rfl
#align prod.snd_inv
Prod.snd_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), p⁻¹.snd = p.snd⁻¹
Prod.snd_inv
#align prod.snd_neg
Prod.snd_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), (-p).snd = -p.snd
Prod.snd_neg
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (a : G) (b : H), -(a, b) = (-a, -b)
to_additive
(attr := simp)] theorem
inv_mk: ∀ [inst : Inv G] [inst_1 : Inv H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)
inv_mk
[
Inv: Type ?u.6195 → Type ?u.6195
Inv
G: Type ?u.6180
G
] [
Inv: Type ?u.6198 → Type ?u.6198
Inv
H: Type ?u.6183
H
] (
a: G
a
:
G: Type ?u.6180
G
) (
b: H
b
:
H: Type ?u.6183
H
) : (
a: G
a
,
b: H
b
)⁻¹ = (
a: G
a
⁻¹,
b: H
b
⁻¹) :=
rfl: ∀ {α : Sort ?u.6311} {a : α}, a = a
rfl
#align prod.inv_mk
Prod.inv_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (a : G) (b : H), (a, b)⁻¹ = (a⁻¹, b⁻¹)
Prod.inv_mk
#align prod.neg_mk
Prod.neg_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (a : G) (b : H), -(a, b) = (-a, -b)
Prod.neg_mk
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), swap (-p) = -swap p
to_additive
(attr := simp)] theorem
swap_inv: ∀ [inst : Inv G] [inst_1 : Inv H] (p : G × H), swap p⁻¹ = (swap p)⁻¹
swap_inv
[
Inv: Type ?u.6417 → Type ?u.6417
Inv
G: Type ?u.6402
G
] [
Inv: Type ?u.6420 → Type ?u.6420
Inv
H: Type ?u.6405
H
] (
p: G × H
p
:
G: Type ?u.6402
G
×
H: Type ?u.6405
H
) :
p: G × H
p
⁻¹.
swap: {α : Type ?u.6466} → {β : Type ?u.6465} → α × β → β × α
swap
=
p: G × H
p
.
swap: {α : Type ?u.6476} → {β : Type ?u.6475} → α × β → β × α
swap
⁻¹ :=
rfl: ∀ {α : Sort ?u.6513} {a : α}, a = a
rfl
#align prod.swap_inv
Prod.swap_inv: ∀ {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst_1 : Inv H] (p : G × H), swap p⁻¹ = (swap p)⁻¹
Prod.swap_inv
#align prod.swap_neg
Prod.swap_neg: ∀ {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst_1 : Neg H] (p : G × H), swap (-p) = -swap p
Prod.swap_neg
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : InvolutiveNeg M] → [inst : InvolutiveNeg N] → InvolutiveNeg (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : InvolutiveInv M] → [inst : InvolutiveInv N] → InvolutiveInv (M × N)
instance
[
InvolutiveInv: Type ?u.6608 → Type ?u.6608
InvolutiveInv
M: Type ?u.6599
M
] [
InvolutiveInv: Type ?u.6611 → Type ?u.6611
InvolutiveInv
N: Type ?u.6602
N
] :
InvolutiveInv: Type ?u.6614 → Type ?u.6614
InvolutiveInv
(
M: Type ?u.6599
M
×
N: Type ?u.6602
N
) := { inv_inv := fun
_: ?m.6786
_
=>
ext: ∀ {α : Type ?u.6788} {β : Type ?u.6789} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
inv_inv: ∀ {G : Type ?u.6799} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv
_: ?m.6800
_
) (
inv_inv: ∀ {G : Type ?u.6821} [inst : InvolutiveInv G] (a : G), a⁻¹⁻¹ = a
inv_inv
_: ?m.6822
_
) } @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : Sub M] → [inst : Sub N] → Sub (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Div M] → [inst : Div N] → Div (M × N)
instance
[
Div: Type ?u.7024 → Type ?u.7024
Div
M: Type ?u.7015
M
] [
Div: Type ?u.7027 → Type ?u.7027
Div
N: Type ?u.7018
N
] :
Div: Type ?u.7030 → Type ?u.7030
Div
(
M: Type ?u.7015
M
×
N: Type ?u.7018
N
) := ⟨fun
p: ?m.7042
p
q: ?m.7045
q
=> ⟨
p: ?m.7042
p
.
1: {α : Type ?u.7061} → {β : Type ?u.7060} → α × β → α
1
/
q: ?m.7045
q
.
1: {α : Type ?u.7065} → {β : Type ?u.7064} → α × β → α
1
,
p: ?m.7042
p
.
2: {α : Type ?u.7109} → {β : Type ?u.7108} → α × β → β
2
/
q: ?m.7045
q
.
2: {α : Type ?u.7113} → {β : Type ?u.7112} → α × β → β
2
⟩⟩ @[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).fst = a.fst - b.fst
to_additive
(attr := simp)] theorem
fst_div: ∀ [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).fst = a.fst / b.fst
fst_div
[
Div: Type ?u.7496 → Type ?u.7496
Div
G: Type ?u.7481
G
] [
Div: Type ?u.7499 → Type ?u.7499
Div
H: Type ?u.7484
H
] (
a: G × H
a
b: G × H
b
:
G: Type ?u.7481
G
×
H: Type ?u.7484
H
) : (
a: G × H
a
/
b: G × H
b
).
1: {α : Type ?u.7585} → {β : Type ?u.7584} → α × β → α
1
=
a: G × H
a
.
1: {α : Type ?u.7594} → {β : Type ?u.7593} → α × β → α
1
/
b: G × H
b
.
1: {α : Type ?u.7598} → {β : Type ?u.7597} → α × β → α
1
:=
rfl: ∀ {α : Sort ?u.7642} {a : α}, a = a
rfl
#align prod.fst_div
Prod.fst_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).fst = a.fst / b.fst
Prod.fst_div
#align prod.fst_sub
Prod.fst_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).fst = a.fst - b.fst
Prod.fst_sub
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).snd = a.snd - b.snd
to_additive
(attr := simp)] theorem
snd_div: ∀ [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).snd = a.snd / b.snd
snd_div
[
Div: Type ?u.7740 → Type ?u.7740
Div
G: Type ?u.7725
G
] [
Div: Type ?u.7743 → Type ?u.7743
Div
H: Type ?u.7728
H
] (
a: G × H
a
b: G × H
b
:
G: Type ?u.7725
G
×
H: Type ?u.7728
H
) : (
a: G × H
a
/
b: G × H
b
).
2: {α : Type ?u.7829} → {β : Type ?u.7828} → α × β → β
2
=
a: G × H
a
.
2: {α : Type ?u.7838} → {β : Type ?u.7837} → α × β → β
2
/
b: G × H
b
.
2: {α : Type ?u.7842} → {β : Type ?u.7841} → α × β → β
2
:=
rfl: ∀ {α : Sort ?u.7886} {a : α}, a = a
rfl
#align prod.snd_div
Prod.snd_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), (a / b).snd = a.snd / b.snd
Prod.snd_div
#align prod.snd_sub
Prod.snd_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), (a - b).snd = a.snd - b.snd
Prod.snd_sub
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (x₁ x₂ : G) (y₁ y₂ : H), (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
to_additive
(attr := simp)] theorem
mk_div_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (x₁ x₂ : G) (y₁ y₂ : H), (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
mk_div_mk
[
Div: Type ?u.7984 → Type ?u.7984
Div
G: Type ?u.7969
G
] [
Div: Type ?u.7987 → Type ?u.7987
Div
H: Type ?u.7972
H
] (
x₁: G
x₁
x₂: G
x₂
:
G: Type ?u.7969
G
) (
y₁: H
y₁
y₂: H
y₂
:
H: Type ?u.7972
H
) : (
x₁: G
x₁
,
y₁: H
y₁
) / (
x₂: G
x₂
,
y₂: H
y₂
) = (
x₁: G
x₁
/
x₂: G
x₂
,
y₁: H
y₁
/
y₂: H
y₂
) :=
rfl: ∀ {α : Sort ?u.8170} {a : α}, a = a
rfl
#align prod.mk_div_mk
Prod.mk_div_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (x₁ x₂ : G) (y₁ y₂ : H), (x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)
Prod.mk_div_mk
#align prod.mk_sub_mk
Prod.mk_sub_mk: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (x₁ x₂ : G) (y₁ y₂ : H), (x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)
Prod.mk_sub_mk
@[
to_additive: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), swap (a - b) = swap a - swap b
to_additive
(attr := simp)] theorem
swap_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), swap (a / b) = swap a / swap b
swap_div
[
Div: Type ?u.8302 → Type ?u.8302
Div
G: Type ?u.8287
G
] [
Div: Type ?u.8305 → Type ?u.8305
Div
H: Type ?u.8290
H
] (
a: G × H
a
b: G × H
b
:
G: Type ?u.8287
G
×
H: Type ?u.8290
H
) : (
a: G × H
a
/
b: G × H
b
).
swap: {α : Type ?u.8391} → {β : Type ?u.8390} → α × β → β × α
swap
=
a: G × H
a
.
swap: {α : Type ?u.8403} → {β : Type ?u.8402} → α × β → β × α
swap
/
b: G × H
b
.
swap: {α : Type ?u.8410} → {β : Type ?u.8409} → α × β → β × α
swap
:=
rfl: ∀ {α : Sort ?u.8477} {a : α}, a = a
rfl
#align prod.swap_div
Prod.swap_div: ∀ {G : Type u_1} {H : Type u_2} [inst : Div G] [inst_1 : Div H] (a b : G × H), swap (a / b) = swap a / swap b
Prod.swap_div
#align prod.swap_sub
Prod.swap_sub: ∀ {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst_1 : Sub H] (a b : G × H), swap (a - b) = swap a - swap b
Prod.swap_sub
instance: {M : Type u_1} → {N : Type u_2} → [inst : MulZeroClass M] → [inst : MulZeroClass N] → MulZeroClass (M × N)
instance
[
MulZeroClass: Type ?u.8589 → Type ?u.8589
MulZeroClass
M: Type ?u.8580
M
] [
MulZeroClass: Type ?u.8592 → Type ?u.8592
MulZeroClass
N: Type ?u.8583
N
] :
MulZeroClass: Type ?u.8595 → Type ?u.8595
MulZeroClass
(
M: Type ?u.8580
M
×
N: Type ?u.8583
N
) := { zero_mul := fun
a: ?m.8805
a
=>
Prod.recOn: ∀ {α : Type ?u.8808} {β : Type ?u.8807} {motive : α × β → Sort ?u.8809} (t : α × β), (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn
a: ?m.8805
a
fun
_: ?m.8880
_
_: ?m.8883
_
=>
mk.inj_iff: ∀ {α : Type ?u.8885} {β : Type ?u.8886} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
zero_mul: ∀ {M₀ : Type ?u.8909} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul
_: ?m.8910
_
,
zero_mul: ∀ {M₀ : Type ?u.8940} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
zero_mul
_: ?m.8941
_
⟩, mul_zero := fun
a: ?m.8845
a
=>
Prod.recOn: ∀ {α : Type ?u.8848} {β : Type ?u.8847} {motive : α × β → Sort ?u.8849} (t : α × β), (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn
a: ?m.8845
a
fun
_: ?m.8979
_
_: ?m.8982
_
=>
mk.inj_iff: ∀ {α : Type ?u.8984} {β : Type ?u.8985} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
mul_zero: ∀ {M₀ : Type ?u.9000} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero
_: ?m.9001
_
,
mul_zero: ∀ {M₀ : Type ?u.9010} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero
_: ?m.9011
_
⟩ } @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddSemigroup M] → [inst : AddSemigroup N] → AddSemigroup (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Semigroup M] → [inst : Semigroup N] → Semigroup (M × N)
instance
[
Semigroup: Type ?u.9130 → Type ?u.9130
Semigroup
M: Type ?u.9121
M
] [
Semigroup: Type ?u.9133 → Type ?u.9133
Semigroup
N: Type ?u.9124
N
] :
Semigroup: Type ?u.9136 → Type ?u.9136
Semigroup
(
M: Type ?u.9121
M
×
N: Type ?u.9124
N
) := { mul_assoc := fun
_: ?m.9522
_
_: ?m.9525
_
_: ?m.9528
_
=>
mk.inj_iff: ∀ {α : Type ?u.9530} {β : Type ?u.9531} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
mul_assoc: ∀ {G : Type ?u.9559} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc
_: ?m.9560
_
_: ?m.9560
_
_: ?m.9560
_
,
mul_assoc: ∀ {G : Type ?u.9595} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc
_: ?m.9596
_
_: ?m.9596
_
_: ?m.9596
_
⟩ } @[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddCommSemigroup G] → [inst : AddCommSemigroup H] → AddCommSemigroup (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : CommSemigroup G] → [inst : CommSemigroup H] → CommSemigroup (G × H)
instance
[
CommSemigroup: Type ?u.9826 → Type ?u.9826
CommSemigroup
G: Type ?u.9811
G
] [
CommSemigroup: Type ?u.9829 → Type ?u.9829
CommSemigroup
H: Type ?u.9814
H
] :
CommSemigroup: Type ?u.9832 → Type ?u.9832
CommSemigroup
(
G: Type ?u.9811
G
×
H: Type ?u.9814
H
) := { mul_comm := fun
_: ?m.10202
_
_: ?m.10205
_
=>
mk.inj_iff: ∀ {α : Type ?u.10207} {β : Type ?u.10208} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
mul_comm: ∀ {G : Type ?u.10236} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
_: ?m.10237
_
_: ?m.10237
_
,
mul_comm: ∀ {G : Type ?u.10261} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
_: ?m.10262
_
_: ?m.10262
_
⟩ }
instance: {M : Type u_1} → {N : Type u_2} → [inst : SemigroupWithZero M] → [inst : SemigroupWithZero N] → SemigroupWithZero (M × N)
instance
[
SemigroupWithZero: Type ?u.10474 → Type ?u.10474
SemigroupWithZero
M: Type ?u.10465
M
] [
SemigroupWithZero: Type ?u.10477 → Type ?u.10477
SemigroupWithZero
N: Type ?u.10468
N
] :
SemigroupWithZero: Type ?u.10480 → Type ?u.10480
SemigroupWithZero
(
M: Type ?u.10465
M
×
N: Type ?u.10468
N
) :=
{ zero_mul := : SemigroupWithZero ?m.10487
{
zero_mul
{ zero_mul := : SemigroupWithZero ?m.10487
:=

Goals accomplished! 🐙
A: Type ?u.10453

B: Type ?u.10456

G: Type ?u.10459

H: Type ?u.10462

M: Type ?u.10465

N: Type ?u.10468

P: Type ?u.10471

inst✝¹: SemigroupWithZero M

inst✝: SemigroupWithZero N


∀ (a : M × N), 0 * a = 0

Goals accomplished! 🐙
, mul_zero := : SemigroupWithZero ?m.10487
,
mul_zero
, mul_zero := : SemigroupWithZero ?m.10487
:=

Goals accomplished! 🐙
A: Type ?u.10453

B: Type ?u.10456

G: Type ?u.10459

H: Type ?u.10462

M: Type ?u.10465

N: Type ?u.10468

P: Type ?u.10471

inst✝¹: SemigroupWithZero M

inst✝: SemigroupWithZero N


∀ (a : M × N), a * 0 = 0

Goals accomplished! 🐙
}: SemigroupWithZero ?m.10487
}
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddZeroClass M] → [inst : AddZeroClass N] → AddZeroClass (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : MulOneClass M] → [inst : MulOneClass N] → MulOneClass (M × N)
instance
[
MulOneClass: Type ?u.12227 → Type ?u.12227
MulOneClass
M: Type ?u.12218
M
] [
MulOneClass: Type ?u.12230 → Type ?u.12230
MulOneClass
N: Type ?u.12221
N
] :
MulOneClass: Type ?u.12233 → Type ?u.12233
MulOneClass
(
M: Type ?u.12218
M
×
N: Type ?u.12221
N
) := { one_mul := fun
a: ?m.12762
a
=>
Prod.recOn: ∀ {α : Type ?u.12765} {β : Type ?u.12764} {motive : α × β → Sort ?u.12766} (t : α × β), (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn
a: ?m.12762
a
fun
_: ?m.12837
_
_: ?m.12840
_
=>
mk.inj_iff: ∀ {α : Type ?u.12842} {β : Type ?u.12843} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
one_mul: ∀ {M : Type ?u.12866} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul
_: ?m.12867
_
,
one_mul: ∀ {M : Type ?u.12900} [inst : MulOneClass M] (a : M), 1 * a = a
one_mul
_: ?m.12901
_
⟩, mul_one := fun
a: ?m.12802
a
=>
Prod.recOn: ∀ {α : Type ?u.12805} {β : Type ?u.12804} {motive : α × β → Sort ?u.12806} (t : α × β), (∀ (fst : α) (snd : β), motive (fst, snd)) → motive t
Prod.recOn
a: ?m.12802
a
fun
_: ?m.12942
_
_: ?m.12945
_
=>
mk.inj_iff: ∀ {α : Type ?u.12947} {β : Type ?u.12948} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
mul_one: ∀ {M : Type ?u.12963} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
_: ?m.12964
_
,
mul_one: ∀ {M : Type ?u.12976} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
_: ?m.12977
_
⟩ } @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddMonoid M] → [inst : AddMonoid N] → AddMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst : Monoid N] → Monoid (M × N)
instance
[
Monoid: Type ?u.13214 → Type ?u.13214
Monoid
M: Type ?u.13205
M
] [
Monoid: Type ?u.13217 → Type ?u.13217
Monoid
N: Type ?u.13208
N
] :
Monoid: Type ?u.13220 → Type ?u.13220
Monoid
(
M: Type ?u.13205
M
×
N: Type ?u.13208
N
) := { npow := fun
z: ?m.13601
z
a: ?m.13604
a
=> ⟨
Monoid.npow: {M : Type ?u.13616} → [self : Monoid M] → ℕ → M → M
Monoid.npow
z: ?m.13601
z
a: ?m.13604
a
.
1: {α : Type ?u.13633} → {β : Type ?u.13632} → α × β → α
1
,
Monoid.npow: {M : Type ?u.13642} → [self : Monoid M] → ℕ → M → M
Monoid.npow
z: ?m.13601
z
a: ?m.13604
a
.
2: {α : Type ?u.13659} → {β : Type ?u.13658} → α × β → β
2
⟩, npow_zero := fun
z: ?m.13673
z
=>
ext: ∀ {α : Type ?u.13675} {β : Type ?u.13676} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
Monoid.npow_zero: ∀ {M : Type ?u.13688} [self : Monoid M] (x : M), Monoid.npow 0 x = 1
Monoid.npow_zero
_: ?m.13689
_
) (
Monoid.npow_zero: ∀ {M : Type ?u.13714} [self : Monoid M] (x : M), Monoid.npow 0 x = 1
Monoid.npow_zero
_: ?m.13715
_
), npow_succ := fun
z: ?m.13746
z
a: ?m.13749
a
=>
ext: ∀ {α : Type ?u.13751} {β : Type ?u.13752} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
Monoid.npow_succ: ∀ {M : Type ?u.13761} [self : Monoid M] (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x
Monoid.npow_succ
_
_: ?m.13762
_
) (
Monoid.npow_succ: ∀ {M : Type ?u.13785} [self : Monoid M] (n : ℕ) (x : M), Monoid.npow (n + 1) x = x * Monoid.npow n x
Monoid.npow_succ
_
_: ?m.13786
_
), one_mul :=

Goals accomplished! 🐙
A: Type ?u.13193

B: Type ?u.13196

G: Type ?u.13199

H: Type ?u.13202

M: Type ?u.13205

N: Type ?u.13208

P: Type ?u.13211

inst✝¹: Monoid M

inst✝: Monoid N


∀ (a : M × N), 1 * a = a

Goals accomplished! 🐙
, mul_one :=

Goals accomplished! 🐙
A: Type ?u.13193

B: Type ?u.13196

G: Type ?u.13199

H: Type ?u.13202

M: Type ?u.13205

N: Type ?u.13208

P: Type ?u.13211

inst✝¹: Monoid M

inst✝: Monoid N


∀ (a : M × N), a * 1 = a

Goals accomplished! 🐙
} @[to_additive
Prod.subNegMonoid: {G : Type u_1} → {H : Type u_2} → [inst : SubNegMonoid G] → [inst : SubNegMonoid H] → SubNegMonoid (G × H)
Prod.subNegMonoid
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : DivInvMonoid G] → [inst : DivInvMonoid H] → DivInvMonoid (G × H)
instance
[
DivInvMonoid: Type ?u.15470 → Type ?u.15470
DivInvMonoid
G: Type ?u.15455
G
] [
DivInvMonoid: Type ?u.15473 → Type ?u.15473
DivInvMonoid
H: Type ?u.15458
H
] :
DivInvMonoid: Type ?u.15476 → Type ?u.15476
DivInvMonoid
(
G: Type ?u.15455
G
×
H: Type ?u.15458
H
) := { div_eq_mul_inv := fun
_: ?m.15784
_
_: ?m.15787
_
=>
mk.inj_iff: ∀ {α : Type ?u.15789} {β : Type ?u.15790} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
div_eq_mul_inv: ∀ {G : Type ?u.15818} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv
_: ?m.15819
_
_: ?m.15819
_
,
div_eq_mul_inv: ∀ {G : Type ?u.15853} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv
_: ?m.15854
_
_: ?m.15854
_
⟩, zpow := fun
z: ?m.15896
z
a: ?m.15899
a
=> ⟨
DivInvMonoid.zpow: {G : Type ?u.15909} → [self : DivInvMonoid G] → ℤ → G → G
DivInvMonoid.zpow
z: ?m.15896
z
a: ?m.15899
a
.
1: {α : Type ?u.15923} → {β : Type ?u.15922} → α × β → α
1
,
DivInvMonoid.zpow: {G : Type ?u.15926} → [self : DivInvMonoid G] → ℤ → G → G
DivInvMonoid.zpow
z: ?m.15896
z
a: ?m.15899
a
.
2: {α : Type ?u.15940} → {β : Type ?u.15939} → α × β → β
2
⟩, zpow_zero' := fun
_: ?m.15948
_
=>
ext: ∀ {α : Type ?u.15950} {β : Type ?u.15951} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
DivInvMonoid.zpow_zero': ∀ {G : Type ?u.15960} [self : DivInvMonoid G] (a : G), DivInvMonoid.zpow 0 a = 1
DivInvMonoid.zpow_zero'
_: ?m.15961
_
) (
DivInvMonoid.zpow_zero': ∀ {G : Type ?u.15980} [self : DivInvMonoid G] (a : G), DivInvMonoid.zpow 0 a = 1
DivInvMonoid.zpow_zero'
_: ?m.15981
_
), zpow_succ' := fun
_: ?m.16006
_
_: ?m.16009
_
=>
ext: ∀ {α : Type ?u.16011} {β : Type ?u.16012} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
DivInvMonoid.zpow_succ': ∀ {G : Type ?u.16021} [self : DivInvMonoid G] (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
DivInvMonoid.zpow_succ'
_
_: ?m.16022
_
) (
DivInvMonoid.zpow_succ': ∀ {G : Type ?u.16041} [self : DivInvMonoid G] (n : ℕ) (a : G), DivInvMonoid.zpow (Int.ofNat (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
DivInvMonoid.zpow_succ'
_
_: ?m.16042
_
), zpow_neg' := fun
_: ?m.16065
_
_: ?m.16068
_
=>
ext: ∀ {α : Type ?u.16070} {β : Type ?u.16071} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
DivInvMonoid.zpow_neg': ∀ {G : Type ?u.16080} [self : DivInvMonoid G] (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
DivInvMonoid.zpow_neg'
_
_: ?m.16081
_
) (
DivInvMonoid.zpow_neg': ∀ {G : Type ?u.16101} [self : DivInvMonoid G] (n : ℕ) (a : G), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) a)⁻¹
DivInvMonoid.zpow_neg'
_
_: ?m.16102
_
) } @[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : SubtractionMonoid G] → [inst : SubtractionMonoid H] → SubtractionMonoid (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : DivisionMonoid G] → [inst : DivisionMonoid H] → DivisionMonoid (G × H)
instance
[
DivisionMonoid: Type ?u.16670 → Type ?u.16670
DivisionMonoid
G: Type ?u.16655
G
] [
DivisionMonoid: Type ?u.16673 → Type ?u.16673
DivisionMonoid
H: Type ?u.16658
H
] :
DivisionMonoid: Type ?u.16676 → Type ?u.16676
DivisionMonoid
(
G: Type ?u.16655
G
×
H: Type ?u.16658
H
) := { mul_inv_rev := fun
a: ?m.16756
a
b: ?m.16759
b
=>
ext: ∀ {α : Type ?u.16761} {β : Type ?u.16762} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
mul_inv_rev: ∀ {G : Type ?u.16772} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev
_: ?m.16773
_
_: ?m.16773
_
) (
mul_inv_rev: ∀ {G : Type ?u.16816} [inst : DivisionMonoid G] (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹
mul_inv_rev
_: ?m.16817
_
_: ?m.16817
_
), inv_eq_of_mul := fun
a: ?m.16868
a
b: ?m.16871
b
h: ?m.16874
h
=>
ext: ∀ {α : Type ?u.16876} {β : Type ?u.16877} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
ext
(
inv_eq_of_mul_eq_one_right: ∀ {G : Type ?u.16884} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b
inv_eq_of_mul_eq_one_right
<|
congr_arg: ∀ {α : Sort ?u.16898} {β : Sort ?u.16897} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
fst: {α : Type ?u.16904} → {β : Type ?u.16903} → α × β → α
fst
h: ?m.16874
h
) (
inv_eq_of_mul_eq_one_right: ∀ {G : Type ?u.16915} [inst : DivisionMonoid G] {a b : G}, a * b = 1 → a⁻¹ = b
inv_eq_of_mul_eq_one_right
<|
congr_arg: ∀ {α : Sort ?u.16929} {β : Sort ?u.16928} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg
snd: {α : Type ?u.16935} → {β : Type ?u.16934} → α × β → β
snd
h: ?m.16874
h
), inv_inv :=

Goals accomplished! 🐙
A: Type ?u.16649

B: Type ?u.16652

G: Type ?u.16655

H: Type ?u.16658

M: Type ?u.16661

N: Type ?u.16664

P: Type ?u.16667

inst✝¹: DivisionMonoid G

inst✝: DivisionMonoid H


∀ (x : G × H), x⁻¹⁻¹ = x

Goals accomplished! 🐙
} @[to_additive
SubtractionCommMonoid: {G : Type u_1} → {H : Type u_2} → [inst : _root_.SubtractionCommMonoid G] → [inst : _root_.SubtractionCommMonoid H] → _root_.SubtractionCommMonoid (G × H)
SubtractionCommMonoid
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : DivisionCommMonoid G] → [inst : DivisionCommMonoid H] → DivisionCommMonoid (G × H)
instance
[
DivisionCommMonoid: Type ?u.17831 → Type ?u.17831
DivisionCommMonoid
G: Type ?u.17816
G
] [
DivisionCommMonoid: Type ?u.17834 → Type ?u.17834
DivisionCommMonoid
H: Type ?u.17819
H
] :
DivisionCommMonoid: Type ?u.17837 → Type ?u.17837
DivisionCommMonoid
(
G: Type ?u.17816
G
×
H: Type ?u.17819
H
) := { mul_comm := fun ⟨
g₁: G
g₁
,
h₁: H
h₁
⟩ ⟨_, _⟩ =>

Goals accomplished! 🐙
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, snd✝ * h₁) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.17810

B: Type ?u.17813

G: Type ?u.17816

H: Type ?u.17819

M: Type ?u.17822

N: Type ?u.17825

P: Type ?u.17828

inst✝¹: DivisionCommMonoid G

inst✝: DivisionCommMonoid H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)

Goals accomplished! 🐙
} @[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst : AddGroup H] → AddGroup (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : Group G] → [inst : Group H] → Group (G × H)
instance
[
Group: Type ?u.18747 → Type ?u.18747
Group
G: Type ?u.18732
G
] [
Group: Type ?u.18750 → Type ?u.18750
Group
H: Type ?u.18735
H
] :
Group: Type ?u.18753 → Type ?u.18753
Group
(
G: Type ?u.18732
G
×
H: Type ?u.18735
H
) := { mul_left_inv := fun
_: ?m.18814
_
=>
mk.inj_iff: ∀ {α : Type ?u.18816} {β : Type ?u.18817} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
mk.inj_iff
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
⟨
mul_left_inv: ∀ {G : Type ?u.18845} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_inv
_: ?m.18846
_
,
mul_left_inv: ∀ {G : Type ?u.18875} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_inv
_: ?m.18876
_
⟩ } @[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddLeftCancelSemigroup G] → [inst : AddLeftCancelSemigroup H] → AddLeftCancelSemigroup (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : LeftCancelSemigroup G] → [inst : LeftCancelSemigroup H] → LeftCancelSemigroup (G × H)
instance
[
LeftCancelSemigroup: Type ?u.19086 → Type ?u.19086
LeftCancelSemigroup
G: Type ?u.19071
G
] [
LeftCancelSemigroup: Type ?u.19089 → Type ?u.19089
LeftCancelSemigroup
H: Type ?u.19074
H
] :
LeftCancelSemigroup: Type ?u.19092 → Type ?u.19092
LeftCancelSemigroup
(
G: Type ?u.19071
G
×
H: Type ?u.19074
H
) := { mul_left_cancel := fun
_: ?m.19448
_
_: ?m.19451
_
_: ?m.19454
_
h: ?m.19457
h
=>
Prod.ext: ∀ {α : Type ?u.19459} {β : Type ?u.19460} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext
(
mul_left_cancel: ∀ {G : Type ?u.19470} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel
(
Prod.ext_iff: ∀ {α : Type ?u.19533} {β : Type ?u.19534} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
h: ?m.19457
h
).
1: ∀ {a b : Prop}, a ∧ b → a
1
) (
mul_left_cancel: ∀ {G : Type ?u.19758} [inst : Mul G] [inst_1 : IsLeftCancelMul G] {a b c : G}, a * b = a * c → b = c
mul_left_cancel
(
Prod.ext_iff: ∀ {α : Type ?u.19821} {β : Type ?u.19822} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
h: ?m.19457
h
).
2: ∀ {a b : Prop}, a ∧ b → b
2
) } @[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddRightCancelSemigroup G] → [inst : AddRightCancelSemigroup H] → AddRightCancelSemigroup (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : RightCancelSemigroup G] → [inst : RightCancelSemigroup H] → RightCancelSemigroup (G × H)
instance
[
RightCancelSemigroup: Type ?u.20244 → Type ?u.20244
RightCancelSemigroup
G: Type ?u.20229
G
] [
RightCancelSemigroup: Type ?u.20247 → Type ?u.20247
RightCancelSemigroup
H: Type ?u.20232
H
] :
RightCancelSemigroup: Type ?u.20250 → Type ?u.20250
RightCancelSemigroup
(
G: Type ?u.20229
G
×
H: Type ?u.20232
H
) := { mul_right_cancel := fun
_: ?m.20592
_
_: ?m.20595
_
_: ?m.20598
_
h: ?m.20601
h
=>
Prod.ext: ∀ {α : Type ?u.20603} {β : Type ?u.20604} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext
(
mul_right_cancel: ∀ {G : Type ?u.20614} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
mul_right_cancel
(
Prod.ext_iff: ∀ {α : Type ?u.20677} {β : Type ?u.20678} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
h: ?m.20601
h
).
1: ∀ {a b : Prop}, a ∧ b → a
1
) (
mul_right_cancel: ∀ {G : Type ?u.20899} [inst : Mul G] [inst_1 : IsRightCancelMul G] {a b c : G}, a * b = c * b → a = c
mul_right_cancel
(
Prod.ext_iff: ∀ {α : Type ?u.20962} {β : Type ?u.20963} {p q : α × β}, p = q ↔ p.fst = q.fst ∧ p.snd = q.snd
Prod.ext_iff
.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1
h: ?m.20601
h
).
2: ∀ {a b : Prop}, a ∧ b → b
2
) } @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddLeftCancelMonoid M] → [inst : AddLeftCancelMonoid N] → AddLeftCancelMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : LeftCancelMonoid M] → [inst : LeftCancelMonoid N] → LeftCancelMonoid (M × N)
instance
[
LeftCancelMonoid: Type ?u.21382 → Type ?u.21382
LeftCancelMonoid
M: Type ?u.21373
M
] [
LeftCancelMonoid: Type ?u.21385 → Type ?u.21385
LeftCancelMonoid
N: Type ?u.21376
N
] :
LeftCancelMonoid: Type ?u.21388 → Type ?u.21388
LeftCancelMonoid
(
M: Type ?u.21373
M
×
N: Type ?u.21376
N
) :=
{ mul_one := : LeftCancelMonoid ?m.21395
{
mul_one
{ mul_one := : LeftCancelMonoid ?m.21395
:=

Goals accomplished! 🐙
A: Type ?u.21361

B: Type ?u.21364

G: Type ?u.21367

H: Type ?u.21370

M: Type ?u.21373

N: Type ?u.21376

P: Type ?u.21379

inst✝¹: LeftCancelMonoid M

inst✝: LeftCancelMonoid N


∀ (a : M × N), a * 1 = a

Goals accomplished! 🐙
, one_mul := : LeftCancelMonoid ?m.21395
,
one_mul
, one_mul := : LeftCancelMonoid ?m.21395
:=

Goals accomplished! 🐙
A: Type ?u.21361

B: Type ?u.21364

G: Type ?u.21367

H: Type ?u.21370

M: Type ?u.21373

N: Type ?u.21376

P: Type ?u.21379

inst✝¹: LeftCancelMonoid M

inst✝: LeftCancelMonoid N


∀ (a : M × N), 1 * a = a

Goals accomplished! 🐙
}: LeftCancelMonoid ?m.21395
}
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddRightCancelMonoid M] → [inst : AddRightCancelMonoid N] → AddRightCancelMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : RightCancelMonoid M] → [inst : RightCancelMonoid N] → RightCancelMonoid (M × N)
instance
[
RightCancelMonoid: Type ?u.23331 → Type ?u.23331
RightCancelMonoid
M: Type ?u.23322
M
] [
RightCancelMonoid: Type ?u.23334 → Type ?u.23334
RightCancelMonoid
N: Type ?u.23325
N
] :
RightCancelMonoid: Type ?u.23337 → Type ?u.23337
RightCancelMonoid
(
M: Type ?u.23322
M
×
N: Type ?u.23325
N
) :=
{ mul_one := : RightCancelMonoid ?m.23344
{
mul_one
{ mul_one := : RightCancelMonoid ?m.23344
:=

Goals accomplished! 🐙
A: Type ?u.23310

B: Type ?u.23313

G: Type ?u.23316

H: Type ?u.23319

M: Type ?u.23322

N: Type ?u.23325

P: Type ?u.23328

inst✝¹: RightCancelMonoid M

inst✝: RightCancelMonoid N


∀ (a : M × N), a * 1 = a

Goals accomplished! 🐙
, one_mul := : RightCancelMonoid ?m.23344
,
one_mul
, one_mul := : RightCancelMonoid ?m.23344
:=

Goals accomplished! 🐙
A: Type ?u.23310

B: Type ?u.23313

G: Type ?u.23316

H: Type ?u.23319

M: Type ?u.23322

N: Type ?u.23325

P: Type ?u.23328

inst✝¹: RightCancelMonoid M

inst✝: RightCancelMonoid N


∀ (a : M × N), 1 * a = a

Goals accomplished! 🐙
}: RightCancelMonoid ?m.23344
}
@[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddCancelMonoid M] → [inst : AddCancelMonoid N] → AddCancelMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CancelMonoid M] → [inst : CancelMonoid N] → CancelMonoid (M × N)
instance
[
CancelMonoid: Type ?u.25176 → Type ?u.25176
CancelMonoid
M: Type ?u.25167
M
] [
CancelMonoid: Type ?u.25179 → Type ?u.25179
CancelMonoid
N: Type ?u.25170
N
] :
CancelMonoid: Type ?u.25182 → Type ?u.25182
CancelMonoid
(
M: Type ?u.25167
M
×
N: Type ?u.25170
N
) := { mul_right_cancel :=

Goals accomplished! 🐙
A: Type ?u.25155

B: Type ?u.25158

G: Type ?u.25161

H: Type ?u.25164

M: Type ?u.25167

N: Type ?u.25170

P: Type ?u.25173

inst✝¹: CancelMonoid M

inst✝: CancelMonoid N


∀ (a b c : M × N), a * b = c * b → a = c

Goals accomplished! 🐙
} @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddCommMonoid M] → [inst : AddCommMonoid N] → AddCommMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CommMonoid M] → [inst : CommMonoid N] → CommMonoid (M × N)
instance
[
CommMonoid: Type ?u.26364 → Type ?u.26364
CommMonoid
M: Type ?u.26355
M
] [
CommMonoid: Type ?u.26367 → Type ?u.26367
CommMonoid
N: Type ?u.26358
N
] :
CommMonoid: Type ?u.26370 → Type ?u.26370
CommMonoid
(
M: Type ?u.26355
M
×
N: Type ?u.26358
N
) := { mul_comm := fun ⟨
m₁: M
m₁
,
n₁: N
n₁
⟩ ⟨_, _⟩ =>

Goals accomplished! 🐙
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(fst✝ * m₁, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.26343

B: Type ?u.26346

G: Type ?u.26349

H: Type ?u.26352

M: Type ?u.26355

N: Type ?u.26358

P: Type ?u.26361

inst✝¹: CommMonoid M

inst✝: CommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(fst✝ * m₁, snd✝ * n₁) = (fst✝ * m₁, snd✝ * n₁)

Goals accomplished! 🐙
} @[
to_additive: {M : Type u_1} → {N : Type u_2} → [inst : AddCancelCommMonoid M] → [inst : AddCancelCommMonoid N] → AddCancelCommMonoid (M × N)
to_additive
]
instance: {M : Type u_1} → {N : Type u_2} → [inst : CancelCommMonoid M] → [inst : CancelCommMonoid N] → CancelCommMonoid (M × N)
instance
[
CancelCommMonoid: Type ?u.27556 → Type ?u.27556
CancelCommMonoid
M: Type ?u.27547
M
] [
CancelCommMonoid: Type ?u.27559 → Type ?u.27559
CancelCommMonoid
N: Type ?u.27550
N
] :
CancelCommMonoid: Type ?u.27562 → Type ?u.27562
CancelCommMonoid
(
M: Type ?u.27547
M
×
N: Type ?u.27550
N
) := { mul_comm := fun ⟨
m₁: M
m₁
,
n₁: N
n₁
⟩ ⟨_, _⟩ =>

Goals accomplished! 🐙
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁ * fst✝, n₁ * snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁ * fst✝, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(fst✝ * m₁, n₁ * snd✝) = (fst✝ * m₁, snd✝ * n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(m₁, n₁) * (fst✝, snd✝) = (fst✝, snd✝) * (m₁, n₁)
A: Type ?u.27535

B: Type ?u.27538

G: Type ?u.27541

H: Type ?u.27544

M: Type ?u.27547

N: Type ?u.27550

P: Type ?u.27553

inst✝¹: CancelCommMonoid M

inst✝: CancelCommMonoid N

x✝¹, x✝: M × N

m₁: M

n₁: N

fst✝: M

snd✝: N


(fst✝ * m₁, snd✝ * n₁) = (fst✝ * m₁, snd✝ * n₁)

Goals accomplished! 🐙
}
instance: {M : Type u_1} → {N : Type u_2} → [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → MulZeroOneClass (M × N)
instance
[
MulZeroOneClass: Type ?u.28577 → Type ?u.28577
MulZeroOneClass
M: Type ?u.28568
M
] [
MulZeroOneClass: Type ?u.28580 → Type ?u.28580
MulZeroOneClass
N: Type ?u.28571
N
] :
MulZeroOneClass: Type ?u.28583 → Type ?u.28583
MulZeroOneClass
(
M: Type ?u.28568
M
×
N: Type ?u.28571
N
) :=
{ zero_mul := : MulZeroOneClass ?m.28590
{
zero_mul
{ zero_mul := : MulZeroOneClass ?m.28590
:=

Goals accomplished! 🐙
A: Type ?u.28556

B: Type ?u.28559

G: Type ?u.28562

H: Type ?u.28565

M: Type ?u.28568

N: Type ?u.28571

P: Type ?u.28574

inst✝¹: MulZeroOneClass M

inst✝: MulZeroOneClass N


∀ (a : M × N), 0 * a = 0

Goals accomplished! 🐙
, mul_zero := : MulZeroOneClass ?m.28590
,
mul_zero
, mul_zero := : MulZeroOneClass ?m.28590
:=

Goals accomplished! 🐙
A: Type ?u.28556

B: Type ?u.28559

G: Type ?u.28562

H: Type ?u.28565

M: Type ?u.28568

N: Type ?u.28571

P: Type ?u.28574

inst✝¹: MulZeroOneClass M

inst✝: MulZeroOneClass N


∀ (a : M × N), a * 0 = 0

Goals accomplished! 🐙
}: MulZeroOneClass ?m.28590
}
instance: {M : Type u_1} → {N : Type u_2} → [inst : MonoidWithZero M] → [inst : MonoidWithZero N] → MonoidWithZero (M × N)
instance
[
MonoidWithZero: Type ?u.30143 → Type ?u.30143
MonoidWithZero
M: Type ?u.30134
M
] [
MonoidWithZero: Type ?u.30146 → Type ?u.30146
MonoidWithZero
N: Type ?u.30137
N
] :
MonoidWithZero: Type ?u.30149 → Type ?u.30149
MonoidWithZero
(
M: Type ?u.30134
M
×
N: Type ?u.30137
N
) :=
{ zero_mul := : MonoidWithZero ?m.30156
{
zero_mul
{ zero_mul := : MonoidWithZero ?m.30156
:=

Goals accomplished! 🐙
A: Type ?u.30122

B: Type ?u.30125

G: Type ?u.30128

H: Type ?u.30131

M: Type ?u.30134

N: Type ?u.30137

P: Type ?u.30140

inst✝¹: MonoidWithZero M

inst✝: MonoidWithZero N


∀ (a : M × N), 0 * a = 0

Goals accomplished! 🐙
, mul_zero := : MonoidWithZero ?m.30156
,
mul_zero
, mul_zero := : MonoidWithZero ?m.30156
:=

Goals accomplished! 🐙
A: Type ?u.30122

B: Type ?u.30125

G: Type ?u.30128

H: Type ?u.30131

M: Type ?u.30134

N: Type ?u.30137

P: Type ?u.30140

inst✝¹: MonoidWithZero M

inst✝: MonoidWithZero N


∀ (a : M × N), a * 0 = 0

Goals accomplished! 🐙
}: MonoidWithZero ?m.30156
}
instance: {M : Type u_1} → {N : Type u_2} → [inst : CommMonoidWithZero M] → [inst : CommMonoidWithZero N] → CommMonoidWithZero (M × N)
instance
[
CommMonoidWithZero: Type ?u.31564 → Type ?u.31564
CommMonoidWithZero
M: Type ?u.31555
M
] [
CommMonoidWithZero: Type ?u.31567 → Type ?u.31567
CommMonoidWithZero
N: Type ?u.31558
N
] :
CommMonoidWithZero: Type ?u.31570 → Type ?u.31570
CommMonoidWithZero
(
M: Type ?u.31555
M
×
N: Type ?u.31558
N
) :=
{ zero_mul := : CommMonoidWithZero ?m.31577
{
zero_mul
{ zero_mul := : CommMonoidWithZero ?m.31577
:=

Goals accomplished! 🐙
A: Type ?u.31543

B: Type ?u.31546

G: Type ?u.31549

H: Type ?u.31552

M: Type ?u.31555

N: Type ?u.31558

P: Type ?u.31561

inst✝¹: CommMonoidWithZero M

inst✝: CommMonoidWithZero N


∀ (a : M × N), 0 * a = 0

Goals accomplished! 🐙
, mul_zero := : CommMonoidWithZero ?m.31577
,
mul_zero
, mul_zero := : CommMonoidWithZero ?m.31577
:=

Goals accomplished! 🐙
A: Type ?u.31543

B: Type ?u.31546

G: Type ?u.31549

H: Type ?u.31552

M: Type ?u.31555

N: Type ?u.31558

P: Type ?u.31561

inst✝¹: CommMonoidWithZero M

inst✝: CommMonoidWithZero N


∀ (a : M × N), a * 0 = 0

Goals accomplished! 🐙
}: CommMonoidWithZero ?m.31577
}
@[
to_additive: {G : Type u_1} → {H : Type u_2} → [inst : AddCommGroup G] → [inst : AddCommGroup H] → AddCommGroup (G × H)
to_additive
]
instance: {G : Type u_1} → {H : Type u_2} → [inst : CommGroup G] → [inst : CommGroup H] → CommGroup (G × H)
instance
[
CommGroup: Type ?u.32990 → Type ?u.32990
CommGroup
G: Type ?u.32975
G
] [
CommGroup: Type ?u.32993 → Type ?u.32993
CommGroup
H: Type ?u.32978
H
] :
CommGroup: Type ?u.32996 → Type ?u.32996
CommGroup
(
G: Type ?u.32975
G
×
H: Type ?u.32978
H
) := { mul_comm := fun ⟨
g₁: G
g₁
,
h₁: H
h₁
⟩ ⟨_, _⟩ =>

Goals accomplished! 🐙
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁ * fst✝, h₁ * snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁ * fst✝, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, h₁ * snd✝) = (fst✝ * g₁, snd✝ * h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(g₁, h₁) * (fst✝, snd✝) = (fst✝, snd✝) * (g₁, h₁)
A: Type ?u.32969

B: Type ?u.32972

G: Type ?u.32975

H: Type ?u.32978

M: Type ?u.32981

N: Type ?u.32984

P: Type ?u.32987

inst✝¹: CommGroup G

inst✝: CommGroup H

x✝¹, x✝: G × H

g₁: G

h₁: H

fst✝: G

snd✝: H


(fst✝ * g₁, snd✝ * h₁) = (fst✝ * g₁, snd✝ * h₁)

Goals accomplished! 🐙
} end Prod namespace MulHom section Prod variable (
M: ?m.33892
M
N: ?m.33895
N
) [
Mul: Type ?u.33898 → Type ?u.33898
Mul
M: Type ?u.33919
M
] [
Mul: Type ?u.34527 → Type ?u.34527
Mul
N: Type ?u.33922
N
] [
Mul: Type ?u.34530 → Type ?u.34530
Mul
P: Type ?u.33889
P
] /-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `M`.-/ @[
to_additive: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) M
to_additive
"Given additive magmas `A`, `B`, the natural projection homomorphism from `A × B` to `A`"] def
fst: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst
:
M: Type ?u.33919
M
×
N: Type ?u.33922
N
→ₙ*
M: Type ?u.33919
M
:= ⟨
Prod.fst: {α : Type ?u.34030} → {β : Type ?u.34029} → α × β → α
Prod.fst
, fun
_: ?m.34039
_
_: ?m.34042
_
=>
rfl: ∀ {α : Sort ?u.34044} {a : α}, a = a
rfl
⟩ #align mul_hom.fst
MulHom.fst: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
MulHom.fst
#align add_hom.fst
AddHom.fst: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) M
AddHom.fst
/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `N`.-/ @[
to_additive: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) N
to_additive
"Given additive magmas `A`, `B`, the natural projection homomorphism from `A × B` to `B`"] def
snd: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd
:
M: Type ?u.34224
M
×
N: Type ?u.34227
N
→ₙ*
N: Type ?u.34227
N
:= ⟨
Prod.snd: {α : Type ?u.34335} → {β : Type ?u.34334} → α × β → β
Prod.snd
, fun
_: ?m.34344
_
_: ?m.34347
_
=>
rfl: ∀ {α : Sort ?u.34349} {a : α}, a = a
rfl
⟩ #align mul_hom.snd
MulHom.snd: (M : Type u_1) → (N : Type u_2) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
MulHom.snd
#align add_hom.snd
AddHom.snd: (M : Type u_1) → (N : Type u_2) → [inst : Add M] → [inst_1 : Add N] → AddHom (M × N) N
AddHom.snd
variable {
M: ?m.34533
M
N: ?m.34536
N
} @[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.fst M N) = Prod.fst
to_additive
(attr := simp)] theorem
coe_fst: ↑(fst M N) = Prod.fst
coe_fst
: ⇑(
fst: (M : Type ?u.34571) → (N : Type ?u.34570) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst
M: Type ?u.34551
M
N: Type ?u.34554
N
) =
Prod.fst: {α : Type ?u.34764} → {β : Type ?u.34763} → α × β → α
Prod.fst
:=
rfl: ∀ {α : Sort ?u.34819} {a : α}, a = a
rfl
#align mul_hom.coe_fst
MulHom.coe_fst: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ↑(fst M N) = Prod.fst
MulHom.coe_fst
#align add_hom.coe_fst
AddHom.coe_fst: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.fst M N) = Prod.fst
AddHom.coe_fst
@[
to_additive: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.snd M N) = Prod.snd
to_additive
(attr := simp)] theorem
coe_snd: ↑(snd M N) = Prod.snd
coe_snd
: ⇑(
snd: (M : Type ?u.34942) → (N : Type ?u.34941) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd
M: Type ?u.34922
M
N: Type ?u.34925
N
) =
Prod.snd: {α : Type ?u.35135} → {β : Type ?u.35134} → α × β → β
Prod.snd
:=
rfl: ∀ {α : Sort ?u.35190} {a : α}, a = a
rfl
#align mul_hom.coe_snd
MulHom.coe_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N], ↑(snd M N) = Prod.snd
MulHom.coe_snd
#align add_hom.coe_snd
AddHom.coe_snd: ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N], ↑(AddHom.snd M N) = Prod.snd
AddHom.coe_snd
/-- Combine two `MonoidHom`s `f : M →ₙ* N`, `g : M →ₙ* P` into `f.prod g : M →ₙ* (N × P)` given by `(f.prod g) x = (f x, g x)`. -/ @[to_additive
prod: {M : Type u_1} → {N : Type u_2} → {P : Type u_3} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → AddHom M N → AddHom M P → AddHom M (N × P)
prod
"Combine two `AddMonoidHom`s `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)`"] protected def
prod: {M : Type u_1} → {N : Type u_2} → {P : Type u_3} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
(f :
M: Type ?u.35293
M
→ₙ*
N: Type ?u.35296
N
) (g :
M: Type ?u.35293
M
→ₙ*
P: Type ?u.35299
P
) :
M: Type ?u.35293
M
→ₙ*
N: Type ?u.35296
N
×
P: Type ?u.35299
P
where toFun :=
Pi.prod: {I : Type ?u.35402} → {f : I → Type ?u.35401} → {g : I → Type ?u.35400} → ((i : I) → f i) → ((i : I) → g i) → (i : I) → f i × g i
Pi.prod
f g map_mul'
x: ?m.35753
x
y: ?m.35756
y
:=
Prod.ext: ∀ {α : Type ?u.35758} {β : Type ?u.35759} {p q : α × β}, p.fst = q.fst → p.snd = q.snd → p = q
Prod.ext
(f.
map_mul: ∀ {M : Type ?u.35769} {N : Type ?u.35770} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M), ↑f (a * b) = ↑f a * ↑f b
map_mul
x: ?m.35753
x
y: ?m.35756
y
) (g.
map_mul: ∀ {M : Type ?u.35791} {N : Type ?u.35792} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (a b : M), ↑f (a * b) = ↑f a * ↑f b
map_mul
x: ?m.35753
x
y: ?m.35756
y
) #align mul_hom.prod
MulHom.prod: {M : Type u_1} → {N : Type u_2} → {P : Type u_3} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
MulHom.prod
#align add_hom.prod
AddHom.prod: {M : Type u_1} → {N : Type u_2} → {P : Type u_3} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → AddHom M N → AddHom M P → AddHom M (N × P)
AddHom.prod
@[to_additive
coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), ↑(AddHom.prod f g) = Pi.prod ↑f ↑g
coe_prod
] theorem
coe_prod: ∀ (f : M →ₙ* N) (g : M →ₙ* P), ↑(MulHom.prod f g) = Pi.prod ↑f ↑g
coe_prod
(f :
M: Type ?u.36210
M
→ₙ*
N: Type ?u.36213
N
) (g :
M: Type ?u.36210
M
→ₙ*
P: Type ?u.36216
P
) : ⇑(f.
prod: {M : Type ?u.36261} → {N : Type ?u.36260} → {P : Type ?u.36259} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
g) =
Pi.prod: {I : Type ?u.36468} → {f : I → Type ?u.36467} → {g : I → Type ?u.36466} → ((i : I) → f i) → ((i : I) → g i) → (i : I) → f i × g i
Pi.prod
f g :=
rfl: ∀ {α : Sort ?u.36824} {a : α}, a = a
rfl
#align mul_hom.coe_prod
MulHom.coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : M →ₙ* P), ↑(MulHom.prod f g) = Pi.prod ↑f ↑g
MulHom.coe_prod
#align add_hom.coe_prod
AddHom.coe_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), ↑(AddHom.prod f g) = Pi.prod ↑f ↑g
AddHom.coe_prod
@[to_additive (attr := simp)
prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P) (x : M), ↑(AddHom.prod f g) x = (↑f x, ↑g x)
prod_apply
] theorem
prod_apply: ∀ (f : M →ₙ* N) (g : M →ₙ* P) (x : M), ↑(MulHom.prod f g) x = (↑f x, ↑g x)
prod_apply
(f :
M: Type ?u.36904
M
→ₙ*
N: Type ?u.36907
N
) (g :
M: Type ?u.36904
M
→ₙ*
P: Type ?u.36910
P
) (
x: M
x
) : f.
prod: {M : Type ?u.36958} → {N : Type ?u.36957} → {P : Type ?u.36956} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
g
x: ?m.36952
x
= (f
x: ?m.36952
x
, g
x: ?m.36952
x
) :=
rfl: ∀ {α : Sort ?u.37507} {a : α}, a = a
rfl
#align mul_hom.prod_apply
MulHom.prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M), ↑(MulHom.prod f g) x = (↑f x, ↑g x)
MulHom.prod_apply
#align add_hom.prod_apply
AddHom.prod_apply: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P) (x : M), ↑(AddHom.prod f g) x = (↑f x, ↑g x)
AddHom.prod_apply
@[to_additive (attr := simp)
fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f
fst_comp_prod
] theorem
fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : M →ₙ* P), comp (fst N P) (MulHom.prod f g) = f
fst_comp_prod
(f :
M: Type ?u.37662
M
→ₙ*
N: Type ?u.37665
N
) (g :
M: Type ?u.37662
M
→ₙ*
P: Type ?u.37668
P
) : (
fst: (M : Type ?u.37712) → (N : Type ?u.37711) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst
N: Type ?u.37665
N
P: Type ?u.37668
P
).
comp: {M : Type ?u.37717} → {N : Type ?u.37716} → {P : Type ?u.37715} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp
(f.
prod: {M : Type ?u.37739} → {N : Type ?u.37738} → {P : Type ?u.37737} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
g) = f :=
ext: ∀ {M : Type ?u.37824} {N : Type ?u.37825} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, (∀ (x : M), ↑f x = ↑g x) → f = g
ext
fun
_: ?m.37880
_
=>
rfl: ∀ {α : Sort ?u.37882} {a : α}, a = a
rfl
#align mul_hom.fst_comp_prod
MulHom.fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : M →ₙ* P), comp (fst N P) (MulHom.prod f g) = f
MulHom.fst_comp_prod
#align add_hom.fst_comp_prod
AddHom.fst_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f
AddHom.fst_comp_prod
@[to_additive (attr := simp)
snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g
snd_comp_prod
] theorem
snd_comp_prod: ∀ (f : M →ₙ* N) (g : M →ₙ* P), comp (snd N P) (MulHom.prod f g) = g
snd_comp_prod
(f :
M: Type ?u.38036
M
→ₙ*
N: Type ?u.38039
N
) (g :
M: Type ?u.38036
M
→ₙ*
P: Type ?u.38042
P
) : (
snd: (M : Type ?u.38086) → (N : Type ?u.38085) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd
N: Type ?u.38039
N
P: Type ?u.38042
P
).
comp: {M : Type ?u.38091} → {N : Type ?u.38090} → {P : Type ?u.38089} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp
(f.
prod: {M : Type ?u.38113} → {N : Type ?u.38112} → {P : Type ?u.38111} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
g) = g :=
ext: ∀ {M : Type ?u.38198} {N : Type ?u.38199} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, (∀ (x : M), ↑f x = ↑g x) → f = g
ext
fun
_: ?m.38254
_
=>
rfl: ∀ {α : Sort ?u.38256} {a : α}, a = a
rfl
#align mul_hom.snd_comp_prod
MulHom.snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N) (g : M →ₙ* P), comp (snd N P) (MulHom.prod f g) = g
MulHom.snd_comp_prod
#align add_hom.snd_comp_prod
AddHom.snd_comp_prod: ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M N) (g : AddHom M P), AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g
AddHom.snd_comp_prod
@[to_additive (attr := simp)
prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M (N × P)), AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f
prod_unique
] theorem
prod_unique: ∀ (f : M →ₙ* N × P), MulHom.prod (comp (fst N P) f) (comp (snd N P) f) = f
prod_unique
(f :
M: Type ?u.38410
M
→ₙ*
N: Type ?u.38413
N
×
P: Type ?u.38416
P
) : ((
fst: (M : Type ?u.38470) → (N : Type ?u.38469) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
fst
N: Type ?u.38413
N
P: Type ?u.38416
P
).
comp: {M : Type ?u.38483} → {N : Type ?u.38482} → {P : Type ?u.38481} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp
f).
prod: {M : Type ?u.38530} → {N : Type ?u.38529} → {P : Type ?u.38528} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (M →ₙ* N) → (M →ₙ* P) → M →ₙ* N × P
prod
((
snd: (M : Type ?u.38550) → (N : Type ?u.38549) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* N
snd
N: Type ?u.38413
N
P: Type ?u.38416
P
).
comp: {M : Type ?u.38555} → {N : Type ?u.38554} → {P : Type ?u.38553} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* P
comp
f) = f :=
ext: ∀ {M : Type ?u.38608} {N : Type ?u.38609} [inst : Mul M] [inst_1 : Mul N] ⦃f g : M →ₙ* N⦄, (∀ (x : M), ↑f x = ↑g x) → f = g
ext
fun
x: ?m.38664
x
=>

Goals accomplished! 🐙
A: Type ?u.38398

B: Type ?u.38401

G: Type ?u.38404

H: Type ?u.38407

M: Type u_1

N: Type u_3

P: Type u_2

inst✝²: Mul M

inst✝¹: Mul N

inst✝: Mul P

f: M →ₙ* N × P

x: M


↑(MulHom.prod (comp (fst N P) f) (comp (snd N P) f)) x = ↑f x

Goals accomplished! 🐙
#align mul_hom.prod_unique
MulHom.prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N × P), MulHom.prod (comp (fst N P) f) (comp (snd N P) f) = f
MulHom.prod_unique
#align add_hom.prod_unique
AddHom.prod_unique: ∀ {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (f : AddHom M (N × P)), AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f
AddHom.prod_unique
end Prod section Prod_map variable {
M': Type ?u.40314
M'
:
Type _: Type (?u.39705+1)
Type _
} {
N': Type ?u.40317
N'
:
Type _: Type (?u.39708+1)
Type _
} [
Mul: Type ?u.39711 → Type ?u.39711
Mul
M: Type ?u.39696
M
] [
Mul: Type ?u.40649 → Type ?u.40649
Mul
N: Type ?u.39777
N
] [
Mul: Type ?u.41496 → Type ?u.41496
Mul
M': Type ?u.40314
M'
] [
Mul: Type ?u.40329 → Type ?u.40329
Mul
N': Type ?u.40317
N'
] [
Mul: Type ?u.40332 → Type ?u.40332
Mul
P: Type ?u.40311
P
] (