Monoid, group etc structures on `M × N× N` #

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

fst M N : M × N →* M× N →* M→* M, snd M N : M × N →* N× N →* N→* N: projections prod.fst and prod.snd as MonoidHoms;
inl M N : M →* M × N→* M × N× N, inr M N : N →* M × N→* M × N× N: inclusions of first/second monoid into the product;
f.prod g : M →* N × P: sends xto(f x, g x)`;
f.coprod g : M × N →* P× N →* P→* P: sends (x, y) to f x * g y;
f.prodMap g : M × N → M' × N'× N → M' × N'→ M' × N'× 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.

source

ink

instance Prod.instAddSum {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

Add (M × N)

Equations

Prod.instAddSum = { add := fun p q => (p.fst + q.fst, p.snd + q.snd) }

source

ink

instance Prod.instMulProd {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

Mul (M × N)

Equations

Prod.instMulProd = { mul := fun p q => (p.fst * q.fst, p.snd * q.snd) }

source

ink

@[simp]

theorem Prod.fst_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (p : M × N) (q : M × N) :

(p + q).fst = p.fst + q.fst

source

ink

@[simp]

theorem Prod.fst_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (p : M × N) (q : M × N) :

(p * q).fst = p.fst * q.fst

source

ink

@[simp]

theorem Prod.snd_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (p : M × N) (q : M × N) :

(p + q).snd = p.snd + q.snd

source

ink

@[simp]

theorem Prod.snd_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (p : M × N) (q : M × N) :

(p * q).snd = p.snd * q.snd

source

ink

@[simp]

theorem Prod.mk_add_mk {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :

(a₁, b₁) + (a₂, b₂) = (a₁ + a₂, b₁ + b₂)

source

ink

@[simp]

theorem Prod.mk_mul_mk {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (a₁ : M) (a₂ : M) (b₁ : N) (b₂ : N) :

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

source

ink

@[simp]

theorem Prod.swap_add {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (p : M × N) (q : M × N) :

Prod.swap (p + q) = Prod.swap p + Prod.swap q

source

ink

@[simp]

theorem Prod.swap_mul {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (p : M × N) (q : M × N) :

Prod.swap (p * q) = Prod.swap p * Prod.swap q

source

ink

theorem Prod.add_def {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] (p : M × N) (q : M × N) :

p + q = (p.fst + q.fst, p.snd + q.snd)

source

ink

theorem Prod.mul_def {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] (p : M × N) (q : M × N) :

p * q = (p.fst * q.fst, p.snd * q.snd)

source

ink

theorem Prod.zero_mk_add_zero_mk {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : Add N] (b₁ : N) (b₂ : N) :

(0, b₁) + (0, b₂) = (0, b₁ + b₂)

source

ink

theorem Prod.one_mk_mul_one_mk {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Mul N] (b₁ : N) (b₂ : N) :

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

source

ink

theorem Prod.mk_zero_add_mk_zero {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : AddMonoid N] (a₁ : M) (a₂ : M) :

(a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)

source

ink

theorem Prod.mk_one_mul_mk_one {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Monoid N] (a₁ : M) (a₂ : M) :

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

source

ink

instance Prod.instZeroSum {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

Zero (M × N)

Equations

Prod.instZeroSum = { zero := (0, 0) }

source

ink

instance Prod.instOneProd {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

One (M × N)

Equations

Prod.instOneProd = { one := (1, 1) }

source

ink

@[simp]

theorem Prod.fst_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

0.fst = 0

source

ink

@[simp]

theorem Prod.fst_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

1.fst = 1

source

ink

@[simp]

theorem Prod.snd_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

0.snd = 0

source

ink

@[simp]

theorem Prod.snd_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

1.snd = 1

source

ink

theorem Prod.zero_eq_mk {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

0 = (0, 0)

source

ink

theorem Prod.one_eq_mk {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

1 = (1, 1)

source

ink

@[simp]

theorem Prod.mk_eq_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] {x : M} {y : N} :

(x, y) = 0 ↔ x = 0 ∧ y = 0

source

ink

@[simp]

theorem Prod.mk_eq_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] {x : M} {y : N} :

(x, y) = 1 ↔ x = 1 ∧ y = 1

source

ink

@[simp]

theorem Prod.swap_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :

Prod.swap 0 = 0

source

ink

@[simp]

theorem Prod.swap_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :

Prod.swap 1 = 1

source

ink

theorem Prod.fst_add_snd {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (p : M × N) :

(p.fst, 0) + (0, p.snd) = p

source

ink

theorem Prod.fst_mul_snd {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (p : M × N) :

(p.fst, 1) * (1, p.snd) = p

source

ink

instance Prod.instNegSum {M : Type u_1} {N : Type u_2} [inst : Neg M] [inst : Neg N] :

Neg (M × N)

Equations

Prod.instNegSum = { neg := fun p => (-p.fst, -p.snd) }

source

ink

instance Prod.instInvProd {M : Type u_1} {N : Type u_2} [inst : Inv M] [inst : Inv N] :

Inv (M × N)

Equations

Prod.instInvProd = { inv := fun p => (p.fst⁻¹, p.snd⁻¹) }

source

ink

@[simp]

theorem Prod.fst_neg {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst : Neg H] (p : G × H) :

(-p).fst = -p.fst

source

ink

@[simp]

theorem Prod.fst_inv {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst : Inv H] (p : G × H) :

p⁻¹.fst = p.fst⁻¹

source

ink

@[simp]

theorem Prod.snd_neg {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst : Neg H] (p : G × H) :

(-p).snd = -p.snd

source

ink

@[simp]

theorem Prod.snd_inv {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst : Inv H] (p : G × H) :

p⁻¹.snd = p.snd⁻¹

source

ink

@[simp]

theorem Prod.neg_mk {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst : Neg H] (a : G) (b : H) :

-(a, b) = (-a, -b)

source

ink

@[simp]

theorem Prod.inv_mk {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst : Inv H] (a : G) (b : H) :

(a, b)⁻¹ = (a⁻¹, b⁻¹)

source

ink

@[simp]

theorem Prod.swap_neg {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst : Neg H] (p : G × H) :

Prod.swap (-p) = -Prod.swap p

source

ink

@[simp]

theorem Prod.swap_inv {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst : Inv H] (p : G × H) :

Prod.swap p⁻¹ = (Prod.swap p)⁻¹

source

ink

def Prod.instInvolutiveNegSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : InvolutiveNeg M] [inst : InvolutiveNeg N] :

∀ (x : M × N), - -x = x

Equations

(_ : - -x = x) = (_ : - -x = x)

source

ink

instance Prod.instInvolutiveNegSum {M : Type u_1} {N : Type u_2} [inst : InvolutiveNeg M] [inst : InvolutiveNeg N] :

InvolutiveNeg (M × N)

Equations

Prod.instInvolutiveNegSum = InvolutiveNeg.mk (_ : ∀ (x : M × N), - -x = x)

source

ink

instance Prod.instInvolutiveInvProd {M : Type u_1} {N : Type u_2} [inst : InvolutiveInv M] [inst : InvolutiveInv N] :

InvolutiveInv (M × N)

Equations

Prod.instInvolutiveInvProd = InvolutiveInv.mk (_ : ∀ (x : M × N), x⁻¹⁻¹ = x)

source

ink

instance Prod.instSubSum {M : Type u_1} {N : Type u_2} [inst : Sub M] [inst : Sub N] :

Sub (M × N)

Equations

Prod.instSubSum = { sub := fun p q => (p.fst - q.fst, p.snd - q.snd) }

source

ink

instance Prod.instDivProd {M : Type u_1} {N : Type u_2} [inst : Div M] [inst : Div N] :

Div (M × N)

Equations

Prod.instDivProd = { div := fun p q => (p.fst / q.fst, p.snd / q.snd) }

source

ink

@[simp]

theorem Prod.fst_sub {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst : Sub H] (a : G × H) (b : G × H) :

(a - b).fst = a.fst - b.fst

source

ink

@[simp]

theorem Prod.fst_div {G : Type u_1} {H : Type u_2} [inst : Div G] [inst : Div H] (a : G × H) (b : G × H) :

(a / b).fst = a.fst / b.fst

source

ink

@[simp]

theorem Prod.snd_sub {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst : Sub H] (a : G × H) (b : G × H) :

(a - b).snd = a.snd - b.snd

source

ink

@[simp]

theorem Prod.snd_div {G : Type u_1} {H : Type u_2} [inst : Div G] [inst : Div H] (a : G × H) (b : G × H) :

(a / b).snd = a.snd / b.snd

source

ink

@[simp]

theorem Prod.mk_sub_mk {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst : Sub H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :

(x₁, y₁) - (x₂, y₂) = (x₁ - x₂, y₁ - y₂)

source

ink

@[simp]

theorem Prod.mk_div_mk {G : Type u_1} {H : Type u_2} [inst : Div G] [inst : Div H] (x₁ : G) (x₂ : G) (y₁ : H) (y₂ : H) :

(x₁, y₁) / (x₂, y₂) = (x₁ / x₂, y₁ / y₂)

source

ink

@[simp]

theorem Prod.swap_sub {G : Type u_1} {H : Type u_2} [inst : Sub G] [inst : Sub H] (a : G × H) (b : G × H) :

Prod.swap (a - b) = Prod.swap a - Prod.swap b

source

ink

@[simp]

theorem Prod.swap_div {G : Type u_1} {H : Type u_2} [inst : Div G] [inst : Div H] (a : G × H) (b : G × H) :

Prod.swap (a / b) = Prod.swap a / Prod.swap b

source

ink

instance Prod.instMulZeroClassProd {M : Type u_1} {N : Type u_2} [inst : MulZeroClass M] [inst : MulZeroClass N] :

MulZeroClass (M × N)

Equations

Prod.instMulZeroClassProd = MulZeroClass.mk (_ : ∀ (a : M × N), 0 * a = 0) (_ : ∀ (a : M × N), a * 0 = 0)

source

ink

def Prod.instAddSemigroupSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst : AddSemigroup N] :

∀ (x x_1 x_2 : M × N), ((x + x_1 + x_2).fst, (x + x_1 + x_2).snd) = ((x + (x_1 + x_2)).fst, (x + (x_1 + x_2)).snd)

Equations

(_ : ((x + x + x).fst, (x + x + x).snd) = ((x + (x + x)).fst, (x + (x + x)).snd)) = (_ : ((x + x + x).fst, (x + x + x).snd) = ((x + (x + x)).fst, (x + (x + x)).snd))

source

ink

instance Prod.instAddSemigroupSum {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst : AddSemigroup N] :

AddSemigroup (M × N)

Equations

Prod.instAddSemigroupSum = AddSemigroup.mk (_ : ∀ (x x_1 x_2 : M × N), ((x + x_1 + x_2).fst, (x + x_1 + x_2).snd) = ((x + (x_1 + x_2)).fst, (x + (x_1 + x_2)).snd))

source

ink

instance Prod.instSemigroupProd {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst : Semigroup N] :

Semigroup (M × N)

Equations

Prod.instSemigroupProd = Semigroup.mk (_ : ∀ (x x_1 x_2 : M × N), ((x * x_1 * x_2).fst, (x * x_1 * x_2).snd) = ((x * (x_1 * x_2)).fst, (x * (x_1 * x_2)).snd))

source

ink

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

AddCommSemigroup (G × H)

Equations

Prod.instAddCommSemigroupSum = AddCommSemigroup.mk (_ : ∀ (x x_1 : G × H), ((x + x_1).fst, (x + x_1).snd) = ((x_1 + x).fst, (x_1 + x).snd))

source

ink

def Prod.instAddCommSemigroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : AddCommSemigroup G] [inst : AddCommSemigroup H] :

∀ (x x_1 : G × H), ((x + x_1).fst, (x + x_1).snd) = ((x_1 + x).fst, (x_1 + x).snd)

Equations

(_ : ((x + x).fst, (x + x).snd) = ((x + x).fst, (x + x).snd)) = (_ : ((x + x).fst, (x + x).snd) = ((x + x).fst, (x + x).snd))

source

ink

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

CommSemigroup (G × H)

Equations

Prod.instCommSemigroupProd = CommSemigroup.mk (_ : ∀ (x x_1 : G × H), ((x * x_1).fst, (x * x_1).snd) = ((x_1 * x).fst, (x_1 * x).snd))

source

ink

instance Prod.instSemigroupWithZeroProd {M : Type u_1} {N : Type u_2} [inst : SemigroupWithZero M] [inst : SemigroupWithZero N] :

SemigroupWithZero (M × N)

Equations

Prod.instSemigroupWithZeroProd = SemigroupWithZero.mk (_ : ∀ (a : M × N), 0 * a = 0) (_ : ∀ (a : M × N), a * 0 = 0)

source

ink

def Prod.instAddZeroClassSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (a : M × N) :

a + 0 = a

Equations

(_ : a + 0 = a) = (_ : a + 0 = a)

source

ink

instance Prod.instAddZeroClassSum {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddZeroClass (M × N)

Equations

Prod.instAddZeroClassSum = AddZeroClass.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a)

source

ink

def Prod.instAddZeroClassSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (a : M × N) :

0 + a = a

Equations

(_ : 0 + a = a) = (_ : 0 + a = a)

source

ink

instance Prod.instMulOneClassProd {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

MulOneClass (M × N)

Equations

Prod.instMulOneClassProd = MulOneClass.mk (_ : ∀ (a : M × N), 1 * a = a) (_ : ∀ (a : M × N), a * 1 = a)

source

ink

def Prod.instAddMonoidSum.proof_4 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (z : ℕ) (a : M × N) :

(fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) (z + 1) a = a + (fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) z a

Equations

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

source

ink

def Prod.instAddMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (a : M × N) :

0 + a = a

Equations

(_ : ∀ (a : M × N), 0 + a = a) = (_ : ∀ (a : M × N), 0 + a = a)

source

ink

instance Prod.instAddMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] :

AddMonoid (M × N)

Equations

Prod.instAddMonoidSum = AddMonoid.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a) fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)

source

ink

def Prod.instAddMonoidSum.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (z : M × N) :

(fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) 0 z = 0

Equations

(_ : (fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) 0 z = 0) = (_ : (fun z a => (AddMonoid.nsmul z a.fst, AddMonoid.nsmul z a.snd)) 0 z = 0)

source

ink

def Prod.instAddMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (a : M × N) :

a + 0 = a

Equations

(_ : ∀ (a : M × N), a + 0 = a) = (_ : ∀ (a : M × N), a + 0 = a)

source

ink

instance Prod.instMonoidProd {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] :

Monoid (M × N)

Equations

Prod.instMonoidProd = Monoid.mk (_ : ∀ (a : M × N), 1 * a = a) (_ : ∀ (a : M × N), a * 1 = a) fun z a => (Monoid.npow z a.fst, Monoid.npow z a.snd)

source

ink

def Prod.subNegMonoid.proof_2 {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst : SubNegMonoid H] :

∀ (x : G × H), (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) 0 x = 0

Equations

(_ : (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) 0 x = 0) = (_ : (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) 0 x = 0)

source

ink

def Prod.subNegMonoid.proof_3 {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst : SubNegMonoid H] :

∀ (x : ℕ) (x_1 : G × H), (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) (Int.ofNat (Nat.succ x)) x_1 = x_1 + (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) (Int.ofNat x) x_1

Equations

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

source

ink

def Prod.subNegMonoid.proof_1 {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst : SubNegMonoid H] :

∀ (x x_1 : G × H), ((x - x_1).fst, (x - x_1).snd) = ((x + -x_1).fst, (x + -x_1).snd)

Equations

(_ : ((x - x).fst, (x - x).snd) = ((x + -x).fst, (x + -x).snd)) = (_ : ((x - x).fst, (x - x).snd) = ((x + -x).fst, (x + -x).snd))

source

ink

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

SubNegMonoid (G × H)

Equations

Prod.subNegMonoid = SubNegMonoid.mk fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)

source

ink

def Prod.subNegMonoid.proof_4 {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst : SubNegMonoid H] :

∀ (x : ℕ) (x_1 : G × H), (fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) (Int.negSucc x) x_1 = -(fun z a => (SubNegMonoid.zsmul z a.fst, SubNegMonoid.zsmul z a.snd)) (↑(Nat.succ x)) x_1

Equations

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

source

ink

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

DivInvMonoid (G × H)

Equations

Prod.instDivInvMonoidProd = DivInvMonoid.mk fun z a => (DivInvMonoid.zpow z a.fst, DivInvMonoid.zpow z a.snd)

source

ink

def Prod.instDivisionAddMonoidSum.proof_2 {G : Type u_1} {H : Type u_2} [inst : SubtractionMonoid G] [inst : SubtractionMonoid H] (a : G × H) (b : G × H) :

-(a + b) = -b + -a

Equations

(_ : -(a + b) = -b + -a) = (_ : -(a + b) = -b + -a)

source

ink

def Prod.instDivisionAddMonoidSum.proof_3 {G : Type u_1} {H : Type u_2} [inst : SubtractionMonoid G] [inst : SubtractionMonoid H] (a : G × H) (b : G × H) (h : a + b = 0) :

-a = b

Equations

(_ : -a = b) = (_ : -a = b)

source

ink

def Prod.instDivisionAddMonoidSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : SubtractionMonoid G] [inst : SubtractionMonoid H] (a : G × H) :

- -a = a

Equations

(_ : ∀ (a : G × H), - -a = a) = (_ : ∀ (a : G × H), - -a = a)

source

ink

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

SubtractionMonoid (G × H)

Equations

Prod.instDivisionAddMonoidSum = SubtractionMonoid.mk (_ : ∀ (a : G × H), - -a = a) (_ : ∀ (a b : G × H), -(a + b) = -b + -a) (_ : ∀ (a b : G × H), a + b = 0 → -a = b)

source

ink

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

DivisionMonoid (G × H)

Equations

Prod.instDivisionMonoidProd = DivisionMonoid.mk (_ : ∀ (a : G × H), a⁻¹⁻¹ = a) (_ : ∀ (a b : G × H), (a * b)⁻¹ = b⁻¹ * a⁻¹) (_ : ∀ (a b : G × H), a * b = 1 → a⁻¹ = b)

source

ink

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

SubtractionCommMonoid (G × H)

Equations

Prod.SubtractionCommMonoid = SubtractionCommMonoid.mk (_ : ∀ (x x_1 : G × H), x + x_1 = x_1 + x)

source

ink

abbrev Prod.SubtractionCommMonoid.match_1 {G : Type u_1} {H : Type u_2} (motive : G × H → Prop) :

(x : G × H) → ((fst : G) → (snd : H) → motive (fst, snd)) → motive x

Equations

Prod.SubtractionCommMonoid.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd

source

ink

def Prod.SubtractionCommMonoid.proof_1 {G : Type u_1} {H : Type u_2} [inst : SubtractionCommMonoid G] [inst : SubtractionCommMonoid H] :

∀ (x x_1 : G × H), x + x_1 = x_1 + x

Equations

(_ : x + x = x + x) = (_ : x + x = x + x)

source

ink

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

DivisionCommMonoid (G × H)

Equations

Prod.instDivisionCommMonoidProd = DivisionCommMonoid.mk (_ : ∀ (x x_1 : G × H), x * x_1 = x_1 * x)

source

ink

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

AddGroup (G × H)

Equations

Prod.instAddGroupSum = AddGroup.mk (_ : ∀ (x : G × H), ((-x + x).fst, (-x + x).snd) = (0.fst, 0.snd))

source

ink

def Prod.instAddGroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst : AddGroup H] :

∀ (x : G × H), ((-x + x).fst, (-x + x).snd) = (0.fst, 0.snd)

Equations

(_ : ((-x + x).fst, (-x + x).snd) = (0.fst, 0.snd)) = (_ : ((-x + x).fst, (-x + x).snd) = (0.fst, 0.snd))

source

ink

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

Group (G × H)

Equations

Prod.instGroupProd = Group.mk (_ : ∀ (x : G × H), ((x⁻¹ * x).fst, (x⁻¹ * x).snd) = (1.fst, 1.snd))

source

ink

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

AddLeftCancelSemigroup (G × H)

Equations

Prod.instAddLeftCancelSemigroupSum = AddLeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : G × H), x + x_1 = x + x_2 → x_1 = x_2)

source

ink

def Prod.instAddLeftCancelSemigroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : AddLeftCancelSemigroup G] [inst : AddLeftCancelSemigroup H] :

∀ (x x_1 x_2 : G × H), x + x_1 = x + x_2 → x_1 = x_2

Equations

(_ : x = x) = (_ : x = x)

source

ink

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

LeftCancelSemigroup (G × H)

Equations

Prod.instLeftCancelSemigroupProd = LeftCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : G × H), x * x_1 = x * x_2 → x_1 = x_2)

source

ink

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

AddRightCancelSemigroup (G × H)

Equations

Prod.instAddRightCancelSemigroupSum = AddRightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : G × H), x + x_1 = x_2 + x_1 → x = x_2)

source

ink

def Prod.instAddRightCancelSemigroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : AddRightCancelSemigroup G] [inst : AddRightCancelSemigroup H] :

∀ (x x_1 x_2 : G × H), x + x_1 = x_2 + x_1 → x = x_2

Equations

(_ : x = x) = (_ : x = x)

source

ink

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

RightCancelSemigroup (G × H)

Equations

Prod.instRightCancelSemigroupProd = RightCancelSemigroup.mk (_ : ∀ (x x_1 x_2 : G × H), x * x_1 = x_2 * x_1 → x = x_2)

source

ink

def Prod.instAddLeftCancelMonoidSum.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddLeftCancelMonoid M] [inst : AddLeftCancelMonoid N] :

∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x

Equations

(_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)

source

ink

def Prod.instAddLeftCancelMonoidSum.proof_4 {M : Type u_1} {N : Type u_2} [inst : AddLeftCancelMonoid M] [inst : AddLeftCancelMonoid N] :

∀ (n : ℕ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x

Equations

(_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)

source

ink

def Prod.instAddLeftCancelMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddLeftCancelMonoid M] [inst : AddLeftCancelMonoid N] (a : M × N) :

a + 0 = a

Equations

(_ : ∀ (a : M × N), a + 0 = a) = (_ : ∀ (a : M × N), a + 0 = a)

source

ink

instance Prod.instAddLeftCancelMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddLeftCancelMonoid M] [inst : AddLeftCancelMonoid N] :

AddLeftCancelMonoid (M × N)

Equations

Prod.instAddLeftCancelMonoidSum = AddLeftCancelMonoid.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a) nsmulRec

source

ink

def Prod.instAddLeftCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddLeftCancelMonoid M] [inst : AddLeftCancelMonoid N] (a : M × N) :

0 + a = a

Equations

(_ : ∀ (a : M × N), 0 + a = a) = (_ : ∀ (a : M × N), 0 + a = a)

source

ink

instance Prod.instLeftCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : LeftCancelMonoid M] [inst : LeftCancelMonoid N] :

LeftCancelMonoid (M × N)

Equations

Prod.instLeftCancelMonoidProd = LeftCancelMonoid.mk (_ : ∀ (a : M × N), 1 * a = a) (_ : ∀ (a : M × N), a * 1 = a) npowRec

source

ink

def Prod.instAddRightCancelMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddRightCancelMonoid M] [inst : AddRightCancelMonoid N] (a : M × N) :

a + 0 = a

Equations

(_ : ∀ (a : M × N), a + 0 = a) = (_ : ∀ (a : M × N), a + 0 = a)

source

ink

def Prod.instAddRightCancelMonoidSum.proof_4 {M : Type u_1} {N : Type u_2} [inst : AddRightCancelMonoid M] [inst : AddRightCancelMonoid N] :

∀ (n : ℕ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x

Equations

(_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x) = (_ : nsmulRec (n + 1) x = nsmulRec (n + 1) x)

source

ink

def Prod.instAddRightCancelMonoidSum.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddRightCancelMonoid M] [inst : AddRightCancelMonoid N] :

∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x

Equations

(_ : nsmulRec 0 x = nsmulRec 0 x) = (_ : nsmulRec 0 x = nsmulRec 0 x)

source

ink

def Prod.instAddRightCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddRightCancelMonoid M] [inst : AddRightCancelMonoid N] (a : M × N) :

0 + a = a

Equations

(_ : ∀ (a : M × N), 0 + a = a) = (_ : ∀ (a : M × N), 0 + a = a)

source

ink

instance Prod.instAddRightCancelMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddRightCancelMonoid M] [inst : AddRightCancelMonoid N] :

AddRightCancelMonoid (M × N)

Equations

Prod.instAddRightCancelMonoidSum = AddRightCancelMonoid.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a) nsmulRec

source

ink

instance Prod.instRightCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : RightCancelMonoid M] [inst : RightCancelMonoid N] :

RightCancelMonoid (M × N)

Equations

Prod.instRightCancelMonoidProd = RightCancelMonoid.mk (_ : ∀ (a : M × N), 1 * a = a) (_ : ∀ (a : M × N), a * 1 = a) npowRec

source

ink

instance Prod.instAddCancelMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddCancelMonoid M] [inst : AddCancelMonoid N] :

AddCancelMonoid (M × N)

Equations

Prod.instAddCancelMonoidSum = AddCancelMonoid.mk (_ : ∀ (a a_1 a_2 : M × N), a + a_1 = a_2 + a_1 → a = a_2)

source

ink

def Prod.instAddCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddCancelMonoid M] [inst : AddCancelMonoid N] (a : M × N) (a : M × N) (a : M × N) :

a + a = a + a → a = a

Equations

(_ : ∀ (a a_1 a_2 : M × N), a + a_1 = a_2 + a_1 → a = a_2) = (_ : ∀ (a a_1 a_2 : M × N), a + a_1 = a_2 + a_1 → a = a_2)

source

ink

instance Prod.instCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : CancelMonoid M] [inst : CancelMonoid N] :

CancelMonoid (M × N)

Equations

Prod.instCancelMonoidProd = CancelMonoid.mk (_ : ∀ (a a_1 a_2 : M × N), a * a_1 = a_2 * a_1 → a = a_2)

source

ink

def Prod.instAddCommMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid N] :

∀ (x x_1 : M × N), x + x_1 = x_1 + x

Equations

(_ : x + x = x + x) = (_ : x + x = x + x)

source

ink

instance Prod.instAddCommMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid N] :

AddCommMonoid (M × N)

Equations

Prod.instAddCommMonoidSum = AddCommMonoid.mk (_ : ∀ (x x_1 : M × N), x + x_1 = x_1 + x)

source

ink

instance Prod.instCommMonoidProd {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst : CommMonoid N] :

CommMonoid (M × N)

Equations

Prod.instCommMonoidProd = CommMonoid.mk (_ : ∀ (x x_1 : M × N), x * x_1 = x_1 * x)

source

ink

def Prod.instAddCancelCommMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddCancelCommMonoid M] [inst : AddCancelCommMonoid N] :

∀ (x x_1 : M × N), x + x_1 = x_1 + x

Equations

(_ : x + x = x + x) = (_ : x + x = x + x)

source

ink

instance Prod.instAddCancelCommMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddCancelCommMonoid M] [inst : AddCancelCommMonoid N] :

AddCancelCommMonoid (M × N)

Equations

Prod.instAddCancelCommMonoidSum = AddCancelCommMonoid.mk (_ : ∀ (x x_1 : M × N), x + x_1 = x_1 + x)

source

ink

instance Prod.instCancelCommMonoidProd {M : Type u_1} {N : Type u_2} [inst : CancelCommMonoid M] [inst : CancelCommMonoid N] :

CancelCommMonoid (M × N)

Equations

Prod.instCancelCommMonoidProd = CancelCommMonoid.mk (_ : ∀ (x x_1 : M × N), x * x_1 = x_1 * x)

source

ink

instance Prod.instMulZeroOneClassProd {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] :

MulZeroOneClass (M × N)

Equations

Prod.instMulZeroOneClassProd = MulZeroOneClass.mk (_ : ∀ (a : M × N), 0 * a = 0) (_ : ∀ (a : M × N), a * 0 = 0)

source

ink

instance Prod.instMonoidWithZeroProd {M : Type u_1} {N : Type u_2} [inst : MonoidWithZero M] [inst : MonoidWithZero N] :

MonoidWithZero (M × N)

Equations

Prod.instMonoidWithZeroProd = MonoidWithZero.mk (_ : ∀ (a : M × N), 0 * a = 0) (_ : ∀ (a : M × N), a * 0 = 0)

source

ink

instance Prod.instCommMonoidWithZeroProd {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst : CommMonoidWithZero N] :

CommMonoidWithZero (M × N)

Equations

Prod.instCommMonoidWithZeroProd = CommMonoidWithZero.mk (_ : ∀ (a : M × N), 0 * a = 0) (_ : ∀ (a : M × N), a * 0 = 0)

source

ink

def Prod.instAddCommGroupSum.proof_1 {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst : AddCommGroup H] :

∀ (x x_1 : G × H), x + x_1 = x_1 + x

Equations

(_ : x + x = x + x) = (_ : x + x = x + x)

source

ink

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

AddCommGroup (G × H)

Equations

Prod.instAddCommGroupSum = AddCommGroup.mk (_ : ∀ (x x_1 : G × H), x + x_1 = x_1 + x)

source

ink

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

CommGroup (G × H)

Equations

Prod.instCommGroupProd = CommGroup.mk (_ : ∀ (x x_1 : G × H), x * x_1 = x_1 * x)

source

ink

def AddHom.fst.proof_1 (M : Type u_1) (N : Type u_2) [inst : Add M] [inst : Add N] :

∀ (x x_1 : M × N), (x + x_1).fst = (x + x_1).fst

Equations

(_ : (x + x).fst = (x + x).fst) = (_ : (x + x).fst = (x + x).fst)

source

ink

def AddHom.fst (M : Type u_1) (N : Type u_2) [inst : Add M] [inst : Add N] :

AddHom (M × N) M

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

Equations

AddHom.fst M N = { toFun := Prod.fst, map_add' := (_ : ∀ (x x_1 : M × N), (x + x_1).fst = (x + x_1).fst) }

source

ink

def MulHom.fst (M : Type u_1) (N : Type u_2) [inst : Mul M] [inst : Mul N] :

M × N →ₙ* M

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

Equations

MulHom.fst M N = { toFun := Prod.fst, map_mul' := (_ : ∀ (x x_1 : M × N), (x * x_1).fst = (x * x_1).fst) }

source

ink

def AddHom.snd.proof_1 (M : Type u_1) (N : Type u_2) [inst : Add M] [inst : Add N] :

∀ (x x_1 : M × N), (x + x_1).snd = (x + x_1).snd

Equations

(_ : (x + x).snd = (x + x).snd) = (_ : (x + x).snd = (x + x).snd)

source

ink

def AddHom.snd (M : Type u_1) (N : Type u_2) [inst : Add M] [inst : Add N] :

AddHom (M × N) N

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

Equations

AddHom.snd M N = { toFun := Prod.snd, map_add' := (_ : ∀ (x x_1 : M × N), (x + x_1).snd = (x + x_1).snd) }

source

ink

def MulHom.snd (M : Type u_1) (N : Type u_2) [inst : Mul M] [inst : Mul N] :

M × N →ₙ* N

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

Equations

MulHom.snd M N = { toFun := Prod.snd, map_mul' := (_ : ∀ (x x_1 : M × N), (x * x_1).snd = (x * x_1).snd) }

source

ink

@[simp]

theorem AddHom.coe_fst {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

↑(AddHom.fst M N) = Prod.fst

source

ink

@[simp]

theorem MulHom.coe_fst {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

↑(MulHom.fst M N) = Prod.fst

source

ink

@[simp]

theorem AddHom.coe_snd {M : Type u_1} {N : Type u_2} [inst : Add M] [inst : Add N] :

↑(AddHom.snd M N) = Prod.snd

source

ink

@[simp]

theorem MulHom.coe_snd {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst : Mul N] :

↑(MulHom.snd M N) = Prod.snd

source

ink

def AddHom.prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) :

AddHom M (N × P)

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

Equations

AddHom.prod f g = { toFun := Pi.prod ↑f ↑g, map_add' := (_ : ∀ (x y : M), Pi.prod (↑f) (↑g) (x + y) = Pi.prod (↑f) (↑g) x + Pi.prod (↑f) (↑g) y) }

source

ink

def AddHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) (x : M) (y : M) :

Pi.prod (↑f) (↑g) (x + y) = Pi.prod (↑f) (↑g) x + Pi.prod (↑f) (↑g) y

Equations

(_ : Pi.prod (↑f) (↑g) (x + y) = Pi.prod (↑f) (↑g) x + Pi.prod (↑f) (↑g) y) = (_ : Pi.prod (↑f) (↑g) (x + y) = Pi.prod (↑f) (↑g) x + Pi.prod (↑f) (↑g) y)

source

ink

def MulHom.prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

M →ₙ* N × P

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

Equations

MulHom.prod f g = { toFun := Pi.prod ↑f ↑g, map_mul' := (_ : ∀ (x y : M), Pi.prod (↑f) (↑g) (x * y) = Pi.prod (↑f) (↑g) x * Pi.prod (↑f) (↑g) y) }

source

ink

theorem AddHom.coe_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) :

↑(AddHom.prod f g) = Pi.prod ↑f ↑g

source

ink

theorem MulHom.coe_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

↑(MulHom.prod f g) = Pi.prod ↑f ↑g

source

ink

@[simp]

theorem AddHom.prod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) (x : M) :

↑(AddHom.prod f g) x = (↑f x, ↑g x)

source

ink

@[simp]

theorem MulHom.prod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) :

↑(MulHom.prod f g) x = (↑f x, ↑g x)

source

ink

@[simp]

theorem AddHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) :

AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f

source

ink

@[simp]

theorem MulHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

MulHom.comp (MulHom.fst N P) (MulHom.prod f g) = f

source

ink

@[simp]

theorem AddHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M N) (g : AddHom M P) :

AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g

source

ink

@[simp]

theorem MulHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : Mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

MulHom.comp (MulHom.snd N P) (MulHom.prod f g) = g

source

ink

@[simp]

theorem AddHom.prod_unique {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : Add M] [inst : Add N] [inst : Add P] (f : AddHom M (N × P)) :

AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f

source

ink

@[simp]

theorem MulHom.prod_unique {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) :

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

source

ink

def AddHom.prodMap {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Add M] [inst : Add N] [inst : Add M'] [inst : Add N'] (f : AddHom M M') (g : AddHom N N') :

AddHom (M × N) (M' × N')

prod.map as an AddMonoidHom

Equations

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

source

ink

def MulHom.prodMap {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Mul M] [inst : Mul N] [inst : Mul M'] [inst : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

M × N →ₙ* M' × N'

Prod.map as a MonoidHom.

Equations

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

source

ink

theorem AddHom.prodMap_def {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Add M] [inst : Add N] [inst : Add M'] [inst : Add N'] (f : AddHom M M') (g : AddHom N N') :

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

source

ink

theorem MulHom.prodMap_def {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Mul M] [inst : Mul N] [inst : Mul M'] [inst : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

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

source

ink

@[simp]

theorem AddHom.coe_prodMap {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Add M] [inst : Add N] [inst : Add M'] [inst : Add N'] (f : AddHom M M') (g : AddHom N N') :

↑(AddHom.prodMap f g) = Prod.map ↑f ↑g

source

ink

@[simp]

theorem MulHom.coe_prodMap {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : Mul M] [inst : Mul N] [inst : Mul M'] [inst : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

↑(MulHom.prodMap f g) = Prod.map ↑f ↑g

source

ink

theorem AddHom.prod_comp_prodMap {M : Type u_2} {N : Type u_3} {P : Type u_1} {M' : Type u_4} {N' : Type u_5} [inst : Add M] [inst : Add N] [inst : Add M'] [inst : Add N'] [inst : Add P] (f : AddHom P M) (g : AddHom P N) (f' : AddHom M M') (g' : AddHom N N') :

AddHom.comp (AddHom.prodMap f' g') (AddHom.prod f g) = AddHom.prod (AddHom.comp f' f) (AddHom.comp g' g)

source

ink

theorem MulHom.prod_comp_prodMap {M : Type u_2} {N : Type u_3} {P : Type u_1} {M' : Type u_4} {N' : Type u_5} [inst : Mul M] [inst : Mul N] [inst : Mul M'] [inst : Mul N'] [inst : Mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :

MulHom.comp (MulHom.prodMap f' g') (MulHom.prod f g) = MulHom.prod (MulHom.comp f' f) (MulHom.comp g' g)

source

ink

def AddHom.coprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : AddCommSemigroup P] (f : AddHom M P) (g : AddHom N P) :

AddHom (M × N) P

Coproduct of two AddHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2× N) = f p.1 + g p.2.

Equations

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

source

ink

def MulHom.coprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : 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× N) = f p.1 * g p.2.

Equations

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

source

ink

@[simp]

theorem AddHom.coprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst : Add N] [inst : AddCommSemigroup P] (f : AddHom M P) (g : AddHom N P) (p : M × N) :

↑(AddHom.coprod f g) p = ↑f p.fst + ↑g p.snd

source

ink

@[simp]

theorem MulHom.coprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst : Mul N] [inst : CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) :

↑(MulHom.coprod f g) p = ↑f p.fst * ↑g p.snd

source

ink

theorem AddHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_2} [inst : Add M] [inst : Add N] [inst : AddCommSemigroup P] {Q : Type u_1} [inst : AddCommSemigroup Q] (h : AddHom P Q) (f : AddHom M P) (g : AddHom N P) :

AddHom.comp h (AddHom.coprod f g) = AddHom.coprod (AddHom.comp h f) (AddHom.comp h g)

source

ink

theorem MulHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_2} [inst : Mul M] [inst : Mul N] [inst : CommSemigroup P] {Q : Type u_1} [inst : CommSemigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :

MulHom.comp h (MulHom.coprod f g) = MulHom.coprod (MulHom.comp h f) (MulHom.comp h g)

source

ink

def AddMonoidHom.fst.proof_1 (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

0.fst = 0.fst

Equations

(_ : 0.fst = 0.fst) = (_ : 0.fst = 0.fst)

source

ink

def AddMonoidHom.fst (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

M × N →+ M

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

Equations

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

source

ink

def AddMonoidHom.fst.proof_2 (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

∀ (x x_1 : M × N), ZeroHom.toFun { toFun := Prod.fst, map_zero' := (_ : 0.fst = 0.fst) } (x + x_1) = ZeroHom.toFun { toFun := Prod.fst, map_zero' := (_ : 0.fst = 0.fst) } (x + x_1)

Equations

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

source

ink

def MonoidHom.fst (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst : MulOneClass N] :

M × N →* M

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

Equations

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

source

ink

def AddMonoidHom.snd (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

M × N →+ N

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

Equations

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

source

ink

def AddMonoidHom.snd.proof_2 (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

∀ (x x_1 : M × N), ZeroHom.toFun { toFun := Prod.snd, map_zero' := (_ : 0.snd = 0.snd) } (x + x_1) = ZeroHom.toFun { toFun := Prod.snd, map_zero' := (_ : 0.snd = 0.snd) } (x + x_1)

Equations

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

source

ink

def AddMonoidHom.snd.proof_1 (M : Type u_2) (N : Type u_1) [inst : AddZeroClass M] [inst : AddZeroClass N] :

0.snd = 0.snd

Equations

(_ : 0.snd = 0.snd) = (_ : 0.snd = 0.snd)

source

ink

def MonoidHom.snd (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst : MulOneClass N] :

M × N →* N

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

Equations

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

source

ink

def AddMonoidHom.inl.proof_1 (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

(fun x => (x, 0)) 0 = (fun x => (x, 0)) 0

Equations

(_ : (fun x => (x, 0)) 0 = (fun x => (x, 0)) 0) = (_ : (fun x => (x, 0)) 0 = (fun x => (x, 0)) 0)

source

ink

def AddMonoidHom.inl (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

M →+ M × N

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

Equations

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

source

ink

def AddMonoidHom.inl.proof_2 (M : Type u_2) (N : Type u_1) [inst : AddZeroClass M] [inst : AddZeroClass N] :

∀ (x x_1 : M), ZeroHom.toFun { toFun := fun x => (x, 0), map_zero' := (_ : (fun x => (x, 0)) 0 = (fun x => (x, 0)) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun x => (x, 0), map_zero' := (_ : (fun x => (x, 0)) 0 = (fun x => (x, 0)) 0) } x + ZeroHom.toFun { toFun := fun x => (x, 0), map_zero' := (_ : (fun x => (x, 0)) 0 = (fun x => (x, 0)) 0) } x_1

Equations

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

source

ink

def MonoidHom.inl (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst : MulOneClass N] :

M →* M × N

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

Equations

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

source

ink

def AddMonoidHom.inr (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

N →+ M × N

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

Equations

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

source

ink

def AddMonoidHom.inr.proof_1 (M : Type u_1) (N : Type u_2) [inst : AddZeroClass M] [inst : AddZeroClass N] :

(fun y => (0, y)) 0 = (fun y => (0, y)) 0

Equations

(_ : (fun y => (0, y)) 0 = (fun y => (0, y)) 0) = (_ : (fun y => (0, y)) 0 = (fun y => (0, y)) 0)

source

ink

def AddMonoidHom.inr.proof_2 (M : Type u_2) (N : Type u_1) [inst : AddZeroClass M] [inst : AddZeroClass N] :

∀ (x x_1 : N), ZeroHom.toFun { toFun := fun y => (0, y), map_zero' := (_ : (fun y => (0, y)) 0 = (fun y => (0, y)) 0) } (x + x_1) = ZeroHom.toFun { toFun := fun y => (0, y), map_zero' := (_ : (fun y => (0, y)) 0 = (fun y => (0, y)) 0) } x + ZeroHom.toFun { toFun := fun y => (0, y), map_zero' := (_ : (fun y => (0, y)) 0 = (fun y => (0, y)) 0) } x_1

Equations

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

source

ink

def MonoidHom.inr (M : Type u_1) (N : Type u_2) [inst : MulOneClass M] [inst : MulOneClass N] :

N →* M × N

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

Equations

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

source

ink

@[simp]

theorem AddMonoidHom.coe_fst {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

↑(AddMonoidHom.fst M N) = Prod.fst

source

ink

@[simp]

theorem MonoidHom.coe_fst {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

↑(MonoidHom.fst M N) = Prod.fst

source

ink

@[simp]

theorem AddMonoidHom.coe_snd {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

↑(AddMonoidHom.snd M N) = Prod.snd

source

ink

@[simp]

theorem MonoidHom.coe_snd {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

↑(MonoidHom.snd M N) = Prod.snd

source

ink

@[simp]

theorem AddMonoidHom.inl_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (x : M) :

↑(AddMonoidHom.inl M N) x = (x, 0)

source

ink

@[simp]

theorem MonoidHom.inl_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (x : M) :

↑(MonoidHom.inl M N) x = (x, 1)

source

ink

@[simp]

theorem AddMonoidHom.inr_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (y : N) :

↑(AddMonoidHom.inr M N) y = (0, y)

source

ink

@[simp]

theorem MonoidHom.inr_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (y : N) :

↑(MonoidHom.inr M N) y = (1, y)

source

ink

@[simp]

theorem AddMonoidHom.fst_comp_inl {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddMonoidHom.comp (AddMonoidHom.fst M N) (AddMonoidHom.inl M N) = AddMonoidHom.id M

source

ink

@[simp]

theorem MonoidHom.fst_comp_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.inl M N) = MonoidHom.id M

source

ink

@[simp]

theorem AddMonoidHom.snd_comp_inl {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddMonoidHom.comp (AddMonoidHom.snd M N) (AddMonoidHom.inl M N) = 0

source

ink

@[simp]

theorem MonoidHom.snd_comp_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.inl M N) = 1

source

ink

@[simp]

theorem AddMonoidHom.fst_comp_inr {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddMonoidHom.comp (AddMonoidHom.fst M N) (AddMonoidHom.inr M N) = 0

source

ink

@[simp]

theorem MonoidHom.fst_comp_inr {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.inr M N) = 1

source

ink

@[simp]

theorem AddMonoidHom.snd_comp_inr {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddMonoidHom.comp (AddMonoidHom.snd M N) (AddMonoidHom.inr M N) = AddMonoidHom.id N

source

ink

@[simp]

theorem MonoidHom.snd_comp_inr {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] :

MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.inr M N) = MonoidHom.id N

source

ink

def AddMonoidHom.prod.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M) (y : M) :

ZeroHom.toFun { toFun := Pi.prod ↑f ↑g, map_zero' := (_ : Pi.prod (↑f) (↑g) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := Pi.prod ↑f ↑g, map_zero' := (_ : Pi.prod (↑f) (↑g) 0 = 0) } x + ZeroHom.toFun { toFun := Pi.prod ↑f ↑g, map_zero' := (_ : Pi.prod (↑f) (↑g) 0 = 0) } y

Equations

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

source

ink

def AddMonoidHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) :

Pi.prod (↑f) (↑g) 0 = 0

Equations

(_ : Pi.prod (↑f) (↑g) 0 = 0) = (_ : Pi.prod (↑f) (↑g) 0 = 0)

source

ink

def AddMonoidHom.prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) :

M →+ N × P

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

Equations

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

source

ink

def MonoidHom.prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) (g : M →* P) :

M →* N × P

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

Equations

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

source

ink

theorem AddMonoidHom.coe_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) :

↑(AddMonoidHom.prod f g) = Pi.prod ↑f ↑g

source

ink

theorem MonoidHom.coe_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) (g : M →* P) :

↑(MonoidHom.prod f g) = Pi.prod ↑f ↑g

source

ink

@[simp]

theorem AddMonoidHom.prod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M) :

↑(AddMonoidHom.prod f g) x = (↑f x, ↑g x)

source

ink

@[simp]

theorem MonoidHom.prod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) (g : M →* P) (x : M) :

↑(MonoidHom.prod f g) x = (↑f x, ↑g x)

source

ink

@[simp]

theorem AddMonoidHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) :

AddMonoidHom.comp (AddMonoidHom.fst N P) (AddMonoidHom.prod f g) = f

source

ink

@[simp]

theorem MonoidHom.fst_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) (g : M →* P) :

MonoidHom.comp (MonoidHom.fst N P) (MonoidHom.prod f g) = f

source

ink

@[simp]

theorem AddMonoidHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N) (g : M →+ P) :

AddMonoidHom.comp (AddMonoidHom.snd N P) (AddMonoidHom.prod f g) = g

source

ink

@[simp]

theorem MonoidHom.snd_comp_prod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N) (g : M →* P) :

MonoidHom.comp (MonoidHom.snd N P) (MonoidHom.prod f g) = g

source

ink

@[simp]

theorem AddMonoidHom.prod_unique {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (f : M →+ N × P) :

AddMonoidHom.prod (AddMonoidHom.comp (AddMonoidHom.fst N P) f) (AddMonoidHom.comp (AddMonoidHom.snd N P) f) = f

source

ink

@[simp]

theorem MonoidHom.prod_unique {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (f : M →* N × P) :

MonoidHom.prod (MonoidHom.comp (MonoidHom.fst N P) f) (MonoidHom.comp (MonoidHom.snd N P) f) = f

source

ink

def AddMonoidHom.prodMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

M × N →+ M' × N'

prod.map as an AddHonoidHom

Equations

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

source

ink

def MonoidHom.prodMap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M'] [inst : MulOneClass N'] (f : M →* M') (g : N →* N') :

M × N →* M' × N'

prod.map as a MonoidHom.

Equations

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

source

ink

theorem AddMonoidHom.prodMap_def {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

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

source

ink

theorem MonoidHom.prodMap_def {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M'] [inst : MulOneClass N'] (f : M →* M') (g : N →* N') :

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

source

ink

@[simp]

theorem AddMonoidHom.coe_prodMap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M →+ M') (g : N →+ N') :

↑(AddMonoidHom.prodMap f g) = Prod.map ↑f ↑g

source

ink

@[simp]

theorem MonoidHom.coe_prodMap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M'] [inst : MulOneClass N'] (f : M →* M') (g : N →* N') :

↑(MonoidHom.prodMap f g) = Prod.map ↑f ↑g

source

ink

theorem AddMonoidHom.prod_comp_prodMap {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_4} {N' : Type u_5} [inst : AddZeroClass M'] [inst : AddZeroClass N'] [inst : AddZeroClass P] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :

AddMonoidHom.comp (AddMonoidHom.prodMap f' g') (AddMonoidHom.prod f g) = AddMonoidHom.prod (AddMonoidHom.comp f' f) (AddMonoidHom.comp g' g)

source

ink

theorem MonoidHom.prod_comp_prodMap {M : Type u_2} {N : Type u_3} {P : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {M' : Type u_4} {N' : Type u_5} [inst : MulOneClass M'] [inst : MulOneClass N'] [inst : MulOneClass P] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :

MonoidHom.comp (MonoidHom.prodMap f' g') (MonoidHom.prod f g) = MonoidHom.prod (MonoidHom.comp f' f) (MonoidHom.comp g' g)

source

ink

def AddMonoidHom.coprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : 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× N) = f p.1 + g p.2.

Equations

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

source

ink

def MonoidHom.coprod {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : 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× N) = f p.1 * g p.2.

Equations

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

source

ink

@[simp]

theorem AddMonoidHom.coprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] (f : M →+ P) (g : N →+ P) (p : M × N) :

↑(AddMonoidHom.coprod f g) p = ↑f p.fst + ↑g p.snd

source

ink

@[simp]

theorem MonoidHom.coprod_apply {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] (f : M →* P) (g : N →* P) (p : M × N) :

↑(MonoidHom.coprod f g) p = ↑f p.fst * ↑g p.snd

source

ink

@[simp]

theorem AddMonoidHom.coprod_comp_inl {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] (f : M →+ P) (g : N →+ P) :

AddMonoidHom.comp (AddMonoidHom.coprod f g) (AddMonoidHom.inl M N) = f

source

ink

@[simp]

theorem MonoidHom.coprod_comp_inl {M : Type u_1} {N : Type u_3} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] (f : M →* P) (g : N →* P) :

MonoidHom.comp (MonoidHom.coprod f g) (MonoidHom.inl M N) = f

source

ink

@[simp]

theorem AddMonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] (f : M →+ P) (g : N →+ P) :

AddMonoidHom.comp (AddMonoidHom.coprod f g) (AddMonoidHom.inr M N) = g

source

ink

@[simp]

theorem MonoidHom.coprod_comp_inr {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] (f : M →* P) (g : N →* P) :

MonoidHom.comp (MonoidHom.coprod f g) (MonoidHom.inr M N) = g

source

ink

@[simp]

theorem AddMonoidHom.coprod_unique {M : Type u_2} {N : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] (f : M × N →+ P) :

AddMonoidHom.coprod (AddMonoidHom.comp f (AddMonoidHom.inl M N)) (AddMonoidHom.comp f (AddMonoidHom.inr M N)) = f

source

ink

@[simp]

theorem MonoidHom.coprod_unique {M : Type u_2} {N : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] (f : M × N →* P) :

MonoidHom.coprod (MonoidHom.comp f (MonoidHom.inl M N)) (MonoidHom.comp f (MonoidHom.inr M N)) = f

source

ink

@[simp]

theorem AddMonoidHom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid N] :

AddMonoidHom.coprod (AddMonoidHom.inl M N) (AddMonoidHom.inr M N) = AddMonoidHom.id (M × N)

source

ink

@[simp]

theorem MonoidHom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst : CommMonoid N] :

MonoidHom.coprod (MonoidHom.inl M N) (MonoidHom.inr M N) = MonoidHom.id (M × N)

source

ink

theorem AddMonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddCommMonoid P] {Q : Type u_1} [inst : AddCommMonoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P) :

AddMonoidHom.comp h (AddMonoidHom.coprod f g) = AddMonoidHom.coprod (AddMonoidHom.comp h f) (AddMonoidHom.comp h g)

source

ink

theorem MonoidHom.comp_coprod {M : Type u_3} {N : Type u_4} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : CommMonoid P] {Q : Type u_1} [inst : CommMonoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :

MonoidHom.comp h (MonoidHom.coprod f g) = MonoidHom.coprod (MonoidHom.comp h f) (MonoidHom.comp h g)

source

ink

def AddEquiv.prodComm.proof_1 {M : Type u_1} {N : Type u_2} :

Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun

Equations

(_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) = (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun)

source

ink

def AddEquiv.prodComm {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

M × N ≃+ N × M

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

Equations

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

source

ink

def AddEquiv.prodComm.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

∀ (x x_1 : M × N), Equiv.toFun { toFun := (Equiv.prodComm M N).toFun, invFun := (Equiv.prodComm M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.prodComm M N).toFun, invFun := (Equiv.prodComm M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) } x + Equiv.toFun { toFun := (Equiv.prodComm M N).toFun, invFun := (Equiv.prodComm M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) } x_1

Equations

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

source

ink

def AddEquiv.prodComm.proof_2 {M : Type u_1} {N : Type u_2} :

Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun

Equations

(_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun) = (_ : Function.RightInverse (Equiv.prodComm M N).invFun (Equiv.prodComm M N).toFun)

source

ink

def MulEquiv.prodComm {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

M × N ≃* N × M

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

Equations

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

source

ink

@[simp]

theorem AddEquiv.coe_prodComm {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

↑AddEquiv.prodComm = Prod.swap

source

ink

@[simp]

theorem MulEquiv.coe_prodComm {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

↑MulEquiv.prodComm = Prod.swap

source

ink

@[simp]

theorem AddEquiv.coe_prodComm_symm {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

↑(AddEquiv.symm AddEquiv.prodComm) = Prod.swap

source

ink

@[simp]

theorem MulEquiv.coe_prodComm_symm {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

↑(MulEquiv.symm MulEquiv.prodComm) = Prod.swap

source

ink

def AddEquiv.prodCongr.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') :

Function.RightInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun

Equations

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

source

ink

def AddEquiv.prodCongr {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') :

M × N ≃+ M' × N'

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

Equations

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

source

ink

def AddEquiv.prodCongr.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') :

Function.LeftInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun

Equations

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

source

ink

def AddEquiv.prodCongr.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {M' : Type u_4} {N' : Type u_3} [inst : AddZeroClass M'] [inst : AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') :

∀ (x x_1 : M × N), Equiv.toFun { toFun := (Equiv.prodCongr f.toEquiv g.toEquiv).toFun, invFun := (Equiv.prodCongr f.toEquiv g.toEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.prodCongr f.toEquiv g.toEquiv).toFun, invFun := (Equiv.prodCongr f.toEquiv g.toEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun) } x + Equiv.toFun { toFun := (Equiv.prodCongr f.toEquiv g.toEquiv).toFun, invFun := (Equiv.prodCongr f.toEquiv g.toEquiv).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodCongr f.toEquiv g.toEquiv).invFun (Equiv.prodCongr f.toEquiv g.toEquiv).toFun) } x_1

Equations

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

source

ink

def MulEquiv.prodCongr {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M'] [inst : MulOneClass N'] (f : M ≃* M') (g : N ≃* N') :

M × N ≃* M' × N'

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

Equations

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

source

ink

def AddEquiv.uniqueProd.proof_3 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : Unique N] :

∀ (x x_1 : N × M), Equiv.toFun { toFun := (Equiv.uniqueProd M N).toFun, invFun := (Equiv.uniqueProd M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.uniqueProd M N).toFun, invFun := (Equiv.uniqueProd M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) } (x + x_1)

Equations

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

source

ink

def AddEquiv.uniqueProd {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : Unique N] :

N × M ≃+ M

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

Equations

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

source

ink

def AddEquiv.uniqueProd.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique N] :

Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun

Equations

(_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) = (_ : Function.LeftInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun)

source

ink

def AddEquiv.uniqueProd.proof_2 {M : Type u_1} {N : Type u_2} [inst : Unique N] :

Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun

Equations

(_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun) = (_ : Function.RightInverse (Equiv.uniqueProd M N).invFun (Equiv.uniqueProd M N).toFun)

source

ink

def MulEquiv.uniqueProd {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : Unique N] :

N × M ≃* M

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

Equations

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

source

ink

def AddEquiv.prodUnique {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : Unique N] :

M × N ≃+ M

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

Equations

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

source

ink

def AddEquiv.prodUnique.proof_2 {M : Type u_1} {N : Type u_2} [inst : Unique N] :

Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun

Equations

(_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) = (_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun)

source

ink

def AddEquiv.prodUnique.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : Unique N] :

∀ (x x_1 : M × N), Equiv.toFun { toFun := (Equiv.prodUnique M N).toFun, invFun := (Equiv.prodUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.prodUnique M N).toFun, invFun := (Equiv.prodUnique M N).invFun, left_inv := (_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun), right_inv := (_ : Function.RightInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) } (x + x_1)

Equations

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

source

ink

def AddEquiv.prodUnique.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique N] :

Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun

Equations

(_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun) = (_ : Function.LeftInverse (Equiv.prodUnique M N).invFun (Equiv.prodUnique M N).toFun)

source

ink

def MulEquiv.prodUnique {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : Unique N] :

M × N ≃* M

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

Equations

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

source

ink

abbrev AddEquiv.prodAddUnits.match_1 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (motive : AddUnits M × AddUnits N → Prop) :

(x : AddUnits M × AddUnits N) → ((u₁ : AddUnits M) → (u₂ : AddUnits N) → motive (u₁, u₂)) → motive x

Equations

AddEquiv.prodAddUnits.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd

source

ink

def AddEquiv.prodAddUnits.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (u : AddUnits M × AddUnits N) :

(↑(-u.fst) + ↑u.fst, ↑(-u.snd) + ↑u.snd) = 0

Equations

(_ : (↑(-u.fst) + ↑u.fst, ↑(-u.snd) + ↑u.snd) = 0) = (_ : (↑(-u.fst) + ↑u.fst, ↑(-u.snd) + ↑u.snd) = 0)

source

ink

def AddEquiv.prodAddUnits.proof_4 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] :

∀ (x : AddUnits M × AddUnits N), ↑(AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) ((fun u => { val := (↑u.fst, ↑u.snd), neg := (↑(-u.fst), ↑(-u.snd)), val_neg := (_ : (↑u.fst + ↑(-u.fst), ↑u.snd + ↑(-u.snd)) = 0), neg_val := (_ : (↑(-u.fst) + ↑u.fst, ↑(-u.snd) + ↑u.snd) = 0) }) x) = x

Equations

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

source

ink

def AddEquiv.prodAddUnits.proof_5 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (a : AddUnits (M × N)) (b : AddUnits (M × N)) :

↑(AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) (a + b) = ↑(AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) a + ↑(AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) b

Equations

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

source

ink

def AddEquiv.prodAddUnits {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] :

AddUnits (M × N) ≃+ AddUnits M × AddUnits N

The additive monoid equivalence between additive units of a product of two additive monoids, and the product of the additive units of each additive monoid.

Equations

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

source

ink

def AddEquiv.prodAddUnits.proof_3 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] (u : AddUnits (M × N)) :

Equations

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

source

ink

def AddEquiv.prodAddUnits.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (u : AddUnits M × AddUnits N) :

(↑u.fst + ↑(-u.fst), ↑u.snd + ↑(-u.snd)) = 0

Equations

(_ : (↑u.fst + ↑(-u.fst), ↑u.snd + ↑(-u.snd)) = 0) = (_ : (↑u.fst + ↑(-u.fst), ↑u.snd + ↑(-u.snd)) = 0)

source

ink

def MulEquiv.prodUnits {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : 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.

source

ink

def AddUnits.embedProduct.proof_1 (α : Type u_1) [inst : AddMonoid α] :

(0, { unop := ↑(-0) }) = 0

Equations

(_ : (0, { unop := ↑(-0) }) = 0) = (_ : (0, { unop := ↑(-0) }) = 0)

source

ink

def AddUnits.embedProduct.proof_2 (α : Type u_1) [inst : AddMonoid α] (x : AddUnits α) (y : AddUnits α) :

(↑x + ↑y, { unop := ↑(-(x + y)) }) = (↑x + ↑y, { unop := ↑(-x) } + { unop := ↑(-y) })

Equations

(_ : (↑x + ↑y, { unop := ↑(-(x + y)) }) = (↑x + ↑y, { unop := ↑(-x) } + { unop := ↑(-y) })) = (_ : (↑x + ↑y, { unop := ↑(-(x + y)) }) = (↑x + ↑y, { unop := ↑(-x) } + { unop := ↑(-y) }))

source

ink

def AddUnits.embedProduct (α : Type u_1) [inst : AddMonoid α] :

AddUnits α →+ α × αᵃᵒᵖ

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

Equations

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

source

ink

@[simp]

theorem AddUnits.embedProduct_apply (α : Type u_1) [inst : AddMonoid α] (x : AddUnits α) :

↑(AddUnits.embedProduct α) x = (↑x, { unop := ↑(-x) })

source

ink

@[simp]

theorem Units.embedProduct_apply (α : Type u_1) [inst : Monoid α] (x : αˣ) :

↑(Units.embedProduct α) x = (↑x, { unop := ↑x⁻¹ })

source

ink

def Units.embedProduct (α : Type u_1) [inst : Monoid α] :

αˣ →* α × αᵐᵒᵖ

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

Equations

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

source

ink

theorem AddUnits.embedProduct_injective (α : Type u_1) [inst : AddMonoid α] :

Function.Injective ↑(AddUnits.embedProduct α)

source

ink

theorem Units.embedProduct_injective (α : Type u_1) [inst : Monoid α] :

Function.Injective ↑(Units.embedProduct α)

Multiplication and division as homomorphisms #

source

ink

def addAddHom {α : Type u_1} [inst : AddCommSemigroup α] :

AddHom (α × α) α

Addition as an additive homomorphism.

Equations

addAddHom = { toFun := fun a => a.fst + a.snd, map_add' := (_ : ∀ (x x_1 : α × α), x.fst + x_1.fst + (x.snd + x_1.snd) = x.fst + x.snd + (x_1.fst + x_1.snd)) }

source

ink

def addAddHom.proof_1 {α : Type u_1} [inst : AddCommSemigroup α] :

∀ (x x_1 : α × α), x.fst + x_1.fst + (x.snd + x_1.snd) = x.fst + x.snd + (x_1.fst + x_1.snd)

Equations

(_ : x.fst + x.fst + (x.snd + x.snd) = x.fst + x.snd + (x.fst + x.snd)) = (_ : x.fst + x.fst + (x.snd + x.snd) = x.fst + x.snd + (x.fst + x.snd))

source

ink

@[simp]

theorem mulMulHom_apply {α : Type u_1} [inst : CommSemigroup α] (a : α × α) :

↑mulMulHom a = a.fst * a.snd

source

ink

@[simp]

theorem addAddHom_apply {α : Type u_1} [inst : AddCommSemigroup α] (a : α × α) :

↑addAddHom a = a.fst + a.snd

source

ink

def mulMulHom {α : Type u_1} [inst : CommSemigroup α] :

α × α →ₙ* α

Multiplication as a multiplicative homomorphism.

Equations

mulMulHom = { toFun := fun a => a.fst * a.snd, map_mul' := (_ : ∀ (x x_1 : α × α), x.fst * x_1.fst * (x.snd * x_1.snd) = x.fst * x.snd * (x_1.fst * x_1.snd)) }