Documentation

Mathlib.Algebra.Group.Prod

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:

Main declarations #

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) }
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) }
@[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
@[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
@[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
@[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
@[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₂)
@[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₂)
@[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) :
@[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) :
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)
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)
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₂)
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₂)
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)
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)
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) }
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) }
@[simp]
theorem Prod.fst_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :
0.fst = 0
@[simp]
theorem Prod.fst_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :
1.fst = 1
@[simp]
theorem Prod.snd_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :
0.snd = 0
@[simp]
theorem Prod.snd_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :
1.snd = 1
theorem Prod.zero_eq_mk {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :
0 = (0, 0)
theorem Prod.one_eq_mk {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :
1 = (1, 1)
@[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
@[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
@[simp]
theorem Prod.swap_zero {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst : Zero N] :
@[simp]
theorem Prod.swap_one {M : Type u_1} {N : Type u_2} [inst : One M] [inst : One N] :
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
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
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) }
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⁻¹) }
@[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
@[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⁻¹
@[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
@[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⁻¹
@[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)
@[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⁻¹)
@[simp]
theorem Prod.swap_neg {G : Type u_1} {H : Type u_2} [inst : Neg G] [inst : Neg H] (p : G × H) :
@[simp]
theorem Prod.swap_inv {G : Type u_1} {H : Type u_2} [inst : Inv G] [inst : Inv H] (p : G × H) :
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
instance Prod.instInvolutiveNegSum {M : Type u_1} {N : Type u_2} [inst : InvolutiveNeg M] [inst : InvolutiveNeg N] :
Equations
instance Prod.instInvolutiveInvProd {M : Type u_1} {N : Type u_2} [inst : InvolutiveInv M] [inst : InvolutiveInv N] :
Equations
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) }
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) }
@[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
@[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
@[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
@[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
@[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₂)
@[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₂)
@[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) :
@[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) :
instance Prod.instMulZeroClassProd {M : Type u_1} {N : Type u_2} [inst : MulZeroClass M] [inst : MulZeroClass N] :
Equations
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))
instance Prod.instAddSemigroupSum {M : Type u_1} {N : Type u_2} [inst : AddSemigroup M] [inst : AddSemigroup 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))
instance Prod.instSemigroupProd {M : Type u_1} {N : Type u_2} [inst : Semigroup M] [inst : Semigroup 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))
instance Prod.instAddCommSemigroupSum {G : Type u_1} {H : Type u_2} [inst : AddCommSemigroup G] [inst : AddCommSemigroup 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))
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))
instance Prod.instCommSemigroupProd {G : Type u_1} {H : Type u_2} [inst : CommSemigroup G] [inst : CommSemigroup 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))
instance Prod.instSemigroupWithZeroProd {M : Type u_1} {N : Type u_2} [inst : SemigroupWithZero M] [inst : SemigroupWithZero N] :
Equations
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)
instance Prod.instAddZeroClassSum {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
Equations
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)
instance Prod.instMulOneClassProd {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
Equations
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.
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)
instance Prod.instAddMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] :
Equations
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
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)
instance Prod.instMonoidProd {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] :
Monoid (M × N)
Equations
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
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.
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))
instance Prod.subNegMonoid {G : Type u_1} {H : Type u_2} [inst : SubNegMonoid G] [inst : SubNegMonoid H] :
Equations
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.
instance Prod.instDivInvMonoidProd {G : Type u_1} {H : Type u_2} [inst : DivInvMonoid G] [inst : DivInvMonoid H] :
Equations
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
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)
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)
instance Prod.instDivisionAddMonoidSum {G : Type u_1} {H : Type u_2} [inst : SubtractionMonoid G] [inst : SubtractionMonoid H] :
Equations
instance Prod.instDivisionMonoidProd {G : Type u_1} {H : Type u_2} [inst : DivisionMonoid G] [inst : DivisionMonoid H] :
Equations
Equations
abbrev Prod.SubtractionCommMonoid.match_1 {G : Type u_1} {H : Type u_2} (motive : G × HProp) :
(x : G × H) → ((fst : G) → (snd : H) → motive (fst, snd)) → motive x
Equations
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)
instance Prod.instDivisionCommMonoidProd {G : Type u_1} {H : Type u_2} [inst : DivisionCommMonoid G] [inst : DivisionCommMonoid H] :
Equations
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))
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))
instance Prod.instGroupProd {G : Type u_1} {H : Type u_2} [inst : Group G] [inst : Group H] :
Group (G × H)
Equations
Equations
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_2x_1 = x_2
Equations
  • (_ : x = x) = (_ : x = x)
Equations
Equations
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_1x = x_2
Equations
  • (_ : x = x) = (_ : x = x)
Equations
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)
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)
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)
Equations
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)
instance Prod.instLeftCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : LeftCancelMonoid M] [inst : LeftCancelMonoid N] :
Equations
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)
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)
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)
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)
Equations
instance Prod.instRightCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : RightCancelMonoid M] [inst : RightCancelMonoid N] :
Equations
instance Prod.instAddCancelMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddCancelMonoid M] [inst : AddCancelMonoid N] :
Equations
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 + aa = a
Equations
  • (_ : ∀ (a a_1 a_2 : M × N), a + a_1 = a_2 + a_1a = a_2) = (_ : ∀ (a a_1 a_2 : M × N), a + a_1 = a_2 + a_1a = a_2)
instance Prod.instCancelMonoidProd {M : Type u_1} {N : Type u_2} [inst : CancelMonoid M] [inst : CancelMonoid N] :
Equations
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)
instance Prod.instAddCommMonoidSum {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid N] :
Equations
instance Prod.instCommMonoidProd {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst : CommMonoid N] :
Equations
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)
Equations
instance Prod.instCancelCommMonoidProd {M : Type u_1} {N : Type u_2} [inst : CancelCommMonoid M] [inst : CancelCommMonoid N] :
Equations
instance Prod.instMulZeroOneClassProd {M : Type u_1} {N : Type u_2} [inst : MulZeroOneClass M] [inst : MulZeroOneClass N] :
Equations
instance Prod.instMonoidWithZeroProd {M : Type u_1} {N : Type u_2} [inst : MonoidWithZero M] [inst : MonoidWithZero N] :
Equations
instance Prod.instCommMonoidWithZeroProd {M : Type u_1} {N : Type u_2} [inst : CommMonoidWithZero M] [inst : CommMonoidWithZero N] :
Equations
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)
instance Prod.instAddCommGroupSum {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst : AddCommGroup H] :
Equations
instance Prod.instCommGroupProd {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst : CommGroup H] :
Equations
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)
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) }
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) }
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)
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) }
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) }
@[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
@[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
@[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
@[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
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
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
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
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
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
@[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)
@[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)
@[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) :
@[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) :
@[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) :
@[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) :
@[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)) :
@[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) :
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
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
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') :
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') :
@[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
@[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
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') :
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') :
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
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
@[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
@[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
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) :
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) :
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)
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.
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.
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.
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.
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.
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)
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.
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)
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.
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.
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.
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.
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)
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.
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.
@[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
@[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
@[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
@[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
@[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)
@[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)
@[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)
@[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)
@[simp]
theorem MonoidHom.fst_comp_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
@[simp]
theorem AddMonoidHom.snd_comp_inl {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
@[simp]
theorem MonoidHom.snd_comp_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
@[simp]
theorem AddMonoidHom.fst_comp_inr {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
@[simp]
theorem MonoidHom.fst_comp_inr {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
@[simp]
theorem MonoidHom.snd_comp_inr {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] :
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.
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
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.
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.
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
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
@[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)
@[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)
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
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
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
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') :
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') :
@[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
@[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
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') :
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') :
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
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
@[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
@[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
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[simp]
theorem MonoidHom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] [inst : CommMonoid N] :
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) :
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) :
def AddEquiv.prodComm.proof_1 {M : Type u_1} {N : Type u_2} :
Equations
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.
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.
def AddEquiv.prodComm.proof_2 {M : Type u_1} {N : Type u_2} :
Equations
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.
@[simp]
theorem AddEquiv.coe_prodComm {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
AddEquiv.prodComm = Prod.swap
@[simp]
theorem MulEquiv.coe_prodComm {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
MulEquiv.prodComm = Prod.swap
@[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
@[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
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.
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.
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.
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.
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.
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.
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.
def AddEquiv.uniqueProd.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique N] :
Equations
def AddEquiv.uniqueProd.proof_2 {M : Type u_1} {N : Type u_2} [inst : Unique N] :
Equations
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.
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.
def AddEquiv.prodUnique.proof_2 {M : Type u_1} {N : Type u_2} [inst : Unique N] :
Equations
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.
def AddEquiv.prodUnique.proof_1 {M : Type u_1} {N : Type u_2} [inst : Unique N] :
Equations
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.
abbrev AddEquiv.prodAddUnits.match_1 {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] (motive : AddUnits M × AddUnits NProp) :
(x : AddUnits M × AddUnits N) → ((u₁ : AddUnits M) → (u₂ : AddUnits N) → motive (u₁, u₂)) → motive x
Equations
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)
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.
Equations
  • One or more equations did not get rendered due to their size.
def AddEquiv.prodAddUnits {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] :

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

Equations
  • One or more equations did not get rendered due to their size.
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.
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)
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.
def AddUnits.embedProduct.proof_1 (α : Type u_1) [inst : AddMonoid α] :
(0, { unop := ↑(-0) }) = 0
Equations
  • (_ : (0, { unop := ↑(-0) }) = 0) = (_ : (0, { unop := ↑(-0) }) = 0)
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) }))
def AddUnits.embedProduct (α : Type u_1) [inst : AddMonoid α] :

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.
@[simp]
theorem AddUnits.embedProduct_apply (α : Type u_1) [inst : AddMonoid α] (x : AddUnits α) :
↑(AddUnits.embedProduct α) x = (x, { unop := ↑(-x) })
@[simp]
theorem Units.embedProduct_apply (α : Type u_1) [inst : Monoid α] (x : αˣ) :
↑(Units.embedProduct α) x = (x, { unop := x⁻¹ })
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.

Multiplication and division as homomorphisms #

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)) }
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))
@[simp]
theorem mulMulHom_apply {α : Type u_1} [inst : CommSemigroup α] (a : α × α) :
mulMulHom a = a.fst * a.snd
@[simp]
theorem addAddHom_apply {α : Type u_1} [inst : AddCommSemigroup α] (a : α × α) :
addAddHom a = a.fst + a.snd
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)) }
def addAddMonoidHom.proof_1 {α : Type u_1} [inst : AddCommMonoid α] :
0.fst + 0 = 0.fst
Equations
  • (_ : 0.fst + 0 = 0.fst) = (_ : 0.fst + 0 = 0.fst)
def addAddMonoidHom {α : Type u_1} [inst : AddCommMonoid α] :
α × α →+ α

Addition as an additive monoid homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
def addAddMonoidHom.proof_2 {α : Type u_1} [inst : AddCommMonoid α] (x : α × α) (y : α × α) :
AddHom.toFun addAddHom (x + y) = AddHom.toFun addAddHom x + AddHom.toFun addAddHom y
Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem addAddMonoidHom_apply {α : Type u_1} [inst : AddCommMonoid α] :
∀ (a : α × α), addAddMonoidHom a = AddHom.toFun addAddHom a
@[simp]
theorem mulMonoidHom_apply {α : Type u_1} [inst : CommMonoid α] :
∀ (a : α × α), mulMonoidHom a = MulHom.toFun mulMulHom a
def mulMonoidHom {α : Type u_1} [inst : CommMonoid α] :
α × α →* α

Multiplication as a monoid homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem mulMonoidWithZeroHom_apply {α : Type u_1} [inst : CommMonoidWithZero α] :
∀ (a : α × α), mulMonoidWithZeroHom a = OneHom.toFun (mulMonoidHom) a
def mulMonoidWithZeroHom {α : Type u_1} [inst : CommMonoidWithZero α] :
α × α →*₀ α

Multiplication as a multiplicative homomorphism with zero.

Equations
  • One or more equations did not get rendered due to their size.
def subAddMonoidHom {α : Type u_1} [inst : SubtractionCommMonoid α] :
α × α →+ α

Subtraction as an additive monoid homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
def subAddMonoidHom.proof_2 {α : Type u_1} [inst : SubtractionCommMonoid α] :
∀ (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))
def subAddMonoidHom.proof_1 {α : Type u_1} [inst : SubtractionCommMonoid α] :
0.fst - 0 = 0.fst
Equations
  • (_ : 0.fst - 0 = 0.fst) = (_ : 0.fst - 0 = 0.fst)
@[simp]
theorem divMonoidHom_apply {α : Type u_1} [inst : DivisionCommMonoid α] (a : α × α) :
divMonoidHom a = a.fst / a.snd
@[simp]
theorem subAddMonoidHom_apply {α : Type u_1} [inst : SubtractionCommMonoid α] (a : α × α) :
subAddMonoidHom a = a.fst - a.snd
def divMonoidHom {α : Type u_1} [inst : DivisionCommMonoid α] :
α × α →* α

Division as a monoid homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem divMonoidWithZeroHom_apply {α : Type u_1} [inst : CommGroupWithZero α] (a : α × α) :
divMonoidWithZeroHom a = a.fst / a.snd
def divMonoidWithZeroHom {α : Type u_1} [inst : CommGroupWithZero α] :
α × α →*₀ α

Division as a multiplicative homomorphism with zero.

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