Monoid, group etc structures on M × N

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

• fst M N : M × N →* M, snd M N : M × N →* N: projections Prod.fst and Prod.snd as MonoidHoms;
• inl M N : M →* M × N, inr M N : N →* M × N: inclusions of first/second monoid into the product;
• f.prod g : M →* N × P: sends x to (f x, g x);
• When P is commutative, f.coprod g : M × N →* P sends (x, y) to f x * g y (without the commutativity assumption on P, see MonoidHom.noncommPiCoprod);
• f.prodMap g : M × N → M' × N': prod.map f g as a MonoidHom, sends (x, y) to (f x, g y).

Main declarations

• mulMulHom/mulMonoidHom/mulMonoidWithZeroHom: Multiplication bundled as a multiplicative/monoid/monoid with zero homomorphism.
• divMonoidHom/divMonoidWithZeroHom: Division bundled as a monoid/monoid with zero homomorphism.

instance Prod.instAdd {M : Type u_5} {N : Type u_6} [Add M] [Add N] : Add (M × N)

Equations

• Prod.instAdd = { add := fun (p q : M × N) => (p.1 + q.1, p.2 + q.2) }

instance Prod.instMul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] : Mul (M × N)

Equations

• Prod.instMul = { mul := fun (p q : M × N) => (p.1 * q.1, p.2 * q.2) }

@[simp]

theorem Prod.fst_add {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) : (p + q).1 = p.1 + q.1

@[simp]

theorem Prod.fst_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) : (p * q).1 = p.1 * q.1

@[simp]

theorem Prod.snd_add {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) : (p + q).2 = p.2 + q.2

@[simp]

theorem Prod.snd_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) : (p * q).2 = p.2 * q.2

@[simp]

theorem Prod.mk_add_mk {M : Type u_5} {N : Type u_6} [Add M] [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_5} {N : Type u_6} [Mul M] [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_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) : Prod.swap (p + q) = Prod.swap p + Prod.swap q

@[simp]

theorem Prod.swap_mul {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) : Prod.swap (p * q) = Prod.swap p * Prod.swap q

theorem Prod.add_def {M : Type u_5} {N : Type u_6} [Add M] [Add N] (p : M × N) (q : M × N) : p + q = (p.1 + q.1, p.2 + q.2)

theorem Prod.mul_def {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] (p : M × N) (q : M × N) : p * q = (p.1 * q.1, p.2 * q.2)

theorem Prod.zero_mk_add_zero_mk {M : Type u_5} {N : Type u_6} [AddMonoid M] [Add N] (b₁ : N) (b₂ : N) : (0, b₁) + (0, b₂) = (0, b₁ + b₂)

theorem Prod.one_mk_mul_one_mk {M : Type u_5} {N : Type u_6} [Monoid M] [Mul N] (b₁ : N) (b₂ : N) : (1, b₁) * (1, b₂) = (1, b₁ * b₂)

theorem Prod.mk_zero_add_mk_zero {M : Type u_5} {N : Type u_6} [Add M] [AddMonoid N] (a₁ : M) (a₂ : M) : (a₁, 0) + (a₂, 0) = (a₁ + a₂, 0)

theorem Prod.mk_one_mul_mk_one {M : Type u_5} {N : Type u_6} [Mul M] [Monoid N] (a₁ : M) (a₂ : M) : (a₁, 1) * (a₂, 1) = (a₁ * a₂, 1)

instance Prod.instZero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] : Zero (M × N)

Equations

• Prod.instZero = { zero := (0, 0) }

instance Prod.instOne {M : Type u_5} {N : Type u_6} [One M] [One N] : One (M × N)

Equations

• Prod.instOne = { one := (1, 1) }

@[simp]

theorem Prod.fst_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] : 0.1 = 0

@[simp]

theorem Prod.fst_one {M : Type u_5} {N : Type u_6} [One M] [One N] : 1.1 = 1

@[simp]

theorem Prod.snd_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] : 0.2 = 0

@[simp]

theorem Prod.snd_one {M : Type u_5} {N : Type u_6} [One M] [One N] : 1.2 = 1

theorem Prod.zero_eq_mk {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] : 0 = (0, 0)

theorem Prod.one_eq_mk {M : Type u_5} {N : Type u_6} [One M] [One N] : 1 = (1, 1)

@[simp]

theorem Prod.mk_eq_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] {x : M} {y : N} : (x, y) = 0 ↔ x = 0 ∧ y = 0

@[simp]

theorem Prod.mk_eq_one {M : Type u_5} {N : Type u_6} [One M] [One N] {x : M} {y : N} : (x, y) = 1 ↔ x = 1 ∧ y = 1

@[simp]

theorem Prod.swap_zero {M : Type u_5} {N : Type u_6} [Zero M] [Zero N] : Prod.swap 0 = 0

@[simp]

theorem Prod.swap_one {M : Type u_5} {N : Type u_6} [One M] [One N] : Prod.swap 1 = 1

theorem Prod.fst_add_snd {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] (p : M × N) : (p.1, 0) + (0, p.2) = p

theorem Prod.fst_mul_snd {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] (p : M × N) : (p.1, 1) * (1, p.2) = p

instance Prod.instNeg {M : Type u_5} {N : Type u_6} [Neg M] [Neg N] : Neg (M × N)

Equations

• Prod.instNeg = { neg := fun (p : M × N) => (-p.1, -p.2) }

instance Prod.instInv {M : Type u_5} {N : Type u_6} [Inv M] [Inv N] : Inv (M × N)

Equations

• Prod.instInv = { inv := fun (p : M × N) => (p.1⁻¹, p.2⁻¹) }

@[simp]

theorem Prod.fst_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) : (-p).1 = -p.1

@[simp]

theorem Prod.fst_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) : p⁻¹.1 = p.1⁻¹

@[simp]

theorem Prod.snd_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) : (-p).2 = -p.2

@[simp]

theorem Prod.snd_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) : p⁻¹.2 = p.2⁻¹

@[simp]

theorem Prod.neg_mk {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (a : G) (b : H) : -(a, b) = (-a, -b)

@[simp]

theorem Prod.inv_mk {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (a : G) (b : H) : (a, b)⁻¹ = (a⁻¹, b⁻¹)

@[simp]

theorem Prod.swap_neg {G : Type u_3} {H : Type u_4} [Neg G] [Neg H] (p : G × H) : Prod.swap (-p) = -Prod.swap p

@[simp]

theorem Prod.swap_inv {G : Type u_3} {H : Type u_4} [Inv G] [Inv H] (p : G × H) : Prod.swap p⁻¹ = (Prod.swap p)⁻¹

instance Prod.instInvolutiveNegSum {M : Type u_5} {N : Type u_6} [InvolutiveNeg M] [InvolutiveNeg N] : InvolutiveNeg (M × N)

Equations

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

theorem Prod.instInvolutiveNegSum.proof_1 {M : Type u_1} {N : Type u_2} [InvolutiveNeg M] [InvolutiveNeg N] : ∀ (x : M × N), - -x = x

instance Prod.instInvolutiveInvProd {M : Type u_5} {N : Type u_6} [InvolutiveInv M] [InvolutiveInv N] : InvolutiveInv (M × N)

Equations

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

instance Prod.instSub {M : Type u_5} {N : Type u_6} [Sub M] [Sub N] : Sub (M × N)

Equations

• Prod.instSub = { sub := fun (p q : M × N) => (p.1 - q.1, p.2 - q.2) }

instance Prod.instDiv {M : Type u_5} {N : Type u_6} [Div M] [Div N] : Div (M × N)

Equations

• Prod.instDiv = { div := fun (p q : M × N) => (p.1 / q.1, p.2 / q.2) }

@[simp]

theorem Prod.fst_sub {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) : (a - b).1 = a.1 - b.1

@[simp]

theorem Prod.fst_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) : (a / b).1 = a.1 / b.1

@[simp]

theorem Prod.snd_sub {G : Type u_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) : (a - b).2 = a.2 - b.2

@[simp]

theorem Prod.snd_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) : (a / b).2 = a.2 / b.2

@[simp]

theorem Prod.mk_sub_mk {G : Type u_3} {H : Type u_4} [Sub G] [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_3} {H : Type u_4} [Div G] [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_3} {H : Type u_4} [Sub G] [Sub H] (a : G × H) (b : G × H) : Prod.swap (a - b) = Prod.swap a - Prod.swap b

@[simp]

theorem Prod.swap_div {G : Type u_3} {H : Type u_4} [Div G] [Div H] (a : G × H) (b : G × H) : Prod.swap (a / b) = Prod.swap a / Prod.swap b

instance Prod.instMulZeroClassProd {M : Type u_5} {N : Type u_6} [MulZeroClass M] [MulZeroClass N] : MulZeroClass (M × N)

Equations

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

instance Prod.instAddSemigroup {M : Type u_5} {N : Type u_6} [AddSemigroup M] [AddSemigroup N] : AddSemigroup (M × N)

Equations

• Prod.instAddSemigroup = AddSemigroup.mk (_ : ∀ (x x_1 x_2 : M × N), ((x + x_1).1 + x_2.1, (x + x_1).2 + x_2.2) = (x.1 + (x_1 + x_2).1, x.2 + (x_1 + x_2).2))

theorem Prod.instAddSemigroup.proof_1 {M : Type u_1} {N : Type u_2} [AddSemigroup M] [AddSemigroup N] : ∀ (x x_1 x_2 : M × N), ((x + x_1).1 + x_2.1, (x + x_1).2 + x_2.2) = (x.1 + (x_1 + x_2).1, x.2 + (x_1 + x_2).2)

instance Prod.instSemigroup {M : Type u_5} {N : Type u_6} [Semigroup M] [Semigroup N] : Semigroup (M × N)

Equations

• Prod.instSemigroup = Semigroup.mk (_ : ∀ (x x_1 x_2 : M × N), ((x * x_1).1 * x_2.1, (x * x_1).2 * x_2.2) = (x.1 * (x_1 * x_2).1, x.2 * (x_1 * x_2).2))

theorem Prod.instAddCommSemigroup.proof_1 {G : Type u_1} {H : Type u_2} [AddCommSemigroup G] [AddCommSemigroup H] : ∀ (x x_1 : G × H), (x.1 + x_1.1, x.2 + x_1.2) = (x_1.1 + x.1, x_1.2 + x.2)

instance Prod.instAddCommSemigroup {G : Type u_3} {H : Type u_4} [AddCommSemigroup G] [AddCommSemigroup H] : AddCommSemigroup (G × H)

Equations

• Prod.instAddCommSemigroup = AddCommSemigroup.mk (_ : ∀ (x x_1 : G × H), (x.1 + x_1.1, x.2 + x_1.2) = (x_1.1 + x.1, x_1.2 + x.2))

instance Prod.instCommSemigroup {G : Type u_3} {H : Type u_4} [CommSemigroup G] [CommSemigroup H] : CommSemigroup (G × H)

Equations

• Prod.instCommSemigroup = CommSemigroup.mk (_ : ∀ (x x_1 : G × H), (x.1 * x_1.1, x.2 * x_1.2) = (x_1.1 * x.1, x_1.2 * x.2))

instance Prod.instSemigroupWithZeroProd {M : Type u_5} {N : Type u_6} [SemigroupWithZero M] [SemigroupWithZero N] : SemigroupWithZero (M × N)

Equations

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

theorem Prod.instAddZeroClass.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (a : M × N) : a + 0 = a

theorem Prod.instAddZeroClass.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (a : M × N) : 0 + a = a

instance Prod.instAddZeroClass {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : AddZeroClass (M × N)

Equations

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

instance Prod.instMulOneClass {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : MulOneClass (M × N)

Equations

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

theorem Prod.instAddMonoid.proof_3 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (z : M × N) : (fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) 0 z = 0

instance Prod.instAddMonoid {M : Type u_5} {N : Type u_6} [AddMonoid M] [AddMonoid N] : AddMonoid (M × N)

Equations

• Prod.instAddMonoid = AddMonoid.mk (_ : ∀ (a : M × N), 0 + a = a) (_ : ∀ (a : M × N), a + 0 = a) fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)

theorem Prod.instAddMonoid.proof_4 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (z : ℕ) (a : M × N) : (fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) (z + 1) a = a + (fun (z : ℕ) (a : M × N) => (AddMonoid.nsmul z a.1, AddMonoid.nsmul z a.2)) z a

theorem Prod.instAddMonoid.proof_2 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (a : M × N) : a + 0 = a

theorem Prod.instAddMonoid.proof_1 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (a : M × N) : 0 + a = a

instance Prod.instMonoid {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] : Monoid (M × N)

Equations

• Prod.instMonoid = Monoid.mk (_ : ∀ (a : M × N), 1 * a = a) (_ : ∀ (a : M × N), a * 1 = a) fun (z : ℕ) (a : M × N) => (Monoid.npow z a.1, Monoid.npow z a.2)

theorem Prod.subNegMonoid.proof_2 {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] : ∀ (x : G × H), (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) 0 x = 0

instance Prod.subNegMonoid {G : Type u_3} {H : Type u_4} [SubNegMonoid G] [SubNegMonoid H] : SubNegMonoid (G × H)

Equations

• Prod.subNegMonoid = SubNegMonoid.mk fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)

theorem Prod.subNegMonoid.proof_4 {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] : ∀ (x : ℕ) (x_1 : G × H), (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) (Int.negSucc x) x_1 = -(fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) (↑(Nat.succ x)) x_1

theorem Prod.subNegMonoid.proof_1 {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] : ∀ (x x_1 : G × H), (x.1 - x_1.1, x.2 - x_1.2) = (x.1 + (-x_1).1, x.2 + (-x_1).2)

theorem Prod.subNegMonoid.proof_3 {G : Type u_1} {H : Type u_2} [SubNegMonoid G] [SubNegMonoid H] : ∀ (x : ℕ) (x_1 : G × H), (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) (Int.ofNat (Nat.succ x)) x_1 = x_1 + (fun (z : ℤ) (a : G × H) => (SubNegMonoid.zsmul z a.1, SubNegMonoid.zsmul z a.2)) (Int.ofNat x) x_1

instance Prod.instDivInvMonoidProd {G : Type u_3} {H : Type u_4} [DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H)

Equations

• Prod.instDivInvMonoidProd = DivInvMonoid.mk fun (z : ℤ) (a : G × H) => (DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2)

theorem Prod.instDivisionAddMonoidSum.proof_2 {G : Type u_1} {H : Type u_2} [SubtractionMonoid G] [SubtractionMonoid H] (a : G × H) (b : G × H) : -(a + b) = -b + -a

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

instance Prod.instDivisionAddMonoidSum {G : Type u_3} {H : Type u_4} [SubtractionMonoid G] [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)

theorem Prod.instDivisionAddMonoidSum.proof_1 {G : Type u_1} {H : Type u_2} [SubtractionMonoid G] [SubtractionMonoid H] (a : G × H) : - -a = a

instance Prod.instDivisionMonoidProd {G : Type u_3} {H : Type u_4} [DivisionMonoid G] [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)

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

• (_ : motive x) = (_ : motive x)

instance Prod.SubtractionCommMonoid {G : Type u_3} {H : Type u_4} [SubtractionCommMonoid G] [SubtractionCommMonoid H] : SubtractionCommMonoid (G × H)

Equations

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

theorem Prod.SubtractionCommMonoid.proof_1 {G : Type u_1} {H : Type u_2} [SubtractionCommMonoid G] [SubtractionCommMonoid H] : ∀ (x x_1 : G × H), x + x_1 = x_1 + x

instance Prod.instDivisionCommMonoidProd {G : Type u_3} {H : Type u_4} [DivisionCommMonoid G] [DivisionCommMonoid H] : DivisionCommMonoid (G × H)

Equations

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

instance Prod.instAddGroup {G : Type u_3} {H : Type u_4} [AddGroup G] [AddGroup H] : AddGroup (G × H)

Equations

• Prod.instAddGroup = AddGroup.mk (_ : ∀ (x : G × H), ((-x).1 + x.1, (-x).2 + x.2) = (0, 0))

theorem Prod.instAddGroup.proof_1 {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] : ∀ (x : G × H), ((-x).1 + x.1, (-x).2 + x.2) = (0, 0)

instance Prod.instGroup {G : Type u_3} {H : Type u_4} [Group G] [Group H] : Group (G × H)

Equations

• Prod.instGroup = Group.mk (_ : ∀ (x : G × H), (x⁻¹.1 * x.1, x⁻¹.2 * x.2) = (1, 1))

instance Prod.instIsAddLeftCancelSumInstAdd {G : Type u_3} {H : Type u_4} [Add G] [Add H] [IsLeftCancelAdd G] [IsLeftCancelAdd H] : IsLeftCancelAdd (G × H)

Equations

• (_ : IsLeftCancelAdd (G × H)) = (_ : IsLeftCancelAdd (G × H))

instance Prod.instIsLeftCancelMulProdInstMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [IsLeftCancelMul G] [IsLeftCancelMul H] : IsLeftCancelMul (G × H)

Equations

• (_ : IsLeftCancelMul (G × H)) = (_ : IsLeftCancelMul (G × H))

instance Prod.instIsAddRightCancelSumInstAdd {G : Type u_3} {H : Type u_4} [Add G] [Add H] [IsRightCancelAdd G] [IsRightCancelAdd H] : IsRightCancelAdd (G × H)

Equations

• (_ : IsRightCancelAdd (G × H)) = (_ : IsRightCancelAdd (G × H))

instance Prod.instIsRightCancelMulProdInstMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [IsRightCancelMul G] [IsRightCancelMul H] : IsRightCancelMul (G × H)

Equations

• (_ : IsRightCancelMul (G × H)) = (_ : IsRightCancelMul (G × H))

instance Prod.instIsAddCancelSumInstAdd {G : Type u_3} {H : Type u_4} [Add G] [Add H] [IsCancelAdd G] [IsCancelAdd H] : IsCancelAdd (G × H)

Equations

• (_ : IsCancelAdd (G × H)) = (_ : IsCancelAdd (G × H))

instance Prod.instIsCancelMulProdInstMul {G : Type u_3} {H : Type u_4} [Mul G] [Mul H] [IsCancelMul G] [IsCancelMul H] : IsCancelMul (G × H)

Equations

• (_ : IsCancelMul (G × H)) = (_ : IsCancelMul (G × H))

instance Prod.instAddLeftCancelSemigroupSum {G : Type u_3} {H : Type u_4} [AddLeftCancelSemigroup G] [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)

theorem Prod.instAddLeftCancelSemigroupSum.proof_1 {G : Type u_1} {H : Type u_2} [AddLeftCancelSemigroup G] [AddLeftCancelSemigroup H] : ∀ (x x_1 x_2 : G × H), x + x_1 = x + x_2 → x_1 = x_2

instance Prod.instLeftCancelSemigroupProd {G : Type u_3} {H : Type u_4} [LeftCancelSemigroup G] [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)

theorem Prod.instAddRightCancelSemigroupSum.proof_1 {G : Type u_1} {H : Type u_2} [AddRightCancelSemigroup G] [AddRightCancelSemigroup H] : ∀ (x x_1 x_2 : G × H), x + x_1 = x_2 + x_1 → x = x_2

instance Prod.instAddRightCancelSemigroupSum {G : Type u_3} {H : Type u_4} [AddRightCancelSemigroup G] [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)

instance Prod.instRightCancelSemigroupProd {G : Type u_3} {H : Type u_4} [RightCancelSemigroup G] [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)

theorem Prod.instAddLeftCancelMonoidSum.proof_4 {M : Type u_1} {N : Type u_2} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] : ∀ (n : ℕ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem Prod.instAddLeftCancelMonoidSum.proof_3 {M : Type u_1} {N : Type u_2} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] : ∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x

instance Prod.instAddLeftCancelMonoidSum {M : Type u_5} {N : Type u_6} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] : AddLeftCancelMonoid (M × N)

Equations

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

theorem Prod.instAddLeftCancelMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] (a : M × N) : a + 0 = a

theorem Prod.instAddLeftCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [AddLeftCancelMonoid M] [AddLeftCancelMonoid N] (a : M × N) : 0 + a = a

instance Prod.instLeftCancelMonoidProd {M : Type u_5} {N : Type u_6} [LeftCancelMonoid M] [LeftCancelMonoid N] : LeftCancelMonoid (M × N)

Equations

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

instance Prod.instAddRightCancelMonoidSum {M : Type u_5} {N : Type u_6} [AddRightCancelMonoid M] [AddRightCancelMonoid N] : AddRightCancelMonoid (M × N)

Equations

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

theorem Prod.instAddRightCancelMonoidSum.proof_3 {M : Type u_1} {N : Type u_2} [AddRightCancelMonoid M] [AddRightCancelMonoid N] : ∀ (x : M × N), nsmulRec 0 x = nsmulRec 0 x

theorem Prod.instAddRightCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [AddRightCancelMonoid M] [AddRightCancelMonoid N] (a : M × N) : 0 + a = a

theorem Prod.instAddRightCancelMonoidSum.proof_4 {M : Type u_1} {N : Type u_2} [AddRightCancelMonoid M] [AddRightCancelMonoid N] : ∀ (n : ℕ) (x : M × N), nsmulRec (n + 1) x = nsmulRec (n + 1) x

theorem Prod.instAddRightCancelMonoidSum.proof_2 {M : Type u_1} {N : Type u_2} [AddRightCancelMonoid M] [AddRightCancelMonoid N] (a : M × N) : a + 0 = a

instance Prod.instRightCancelMonoidProd {M : Type u_5} {N : Type u_6} [RightCancelMonoid M] [RightCancelMonoid N] : RightCancelMonoid (M × N)

Equations

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

instance Prod.instAddCancelMonoidSum {M : Type u_5} {N : Type u_6} [AddCancelMonoid M] [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)

theorem Prod.instAddCancelMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [AddCancelMonoid M] [AddCancelMonoid N] (a : M × N) (a : M × N) (a : M × N) : a✝¹ + a✝ = a + a✝ → a✝¹ = a

instance Prod.instCancelMonoidProd {M : Type u_5} {N : Type u_6} [CancelMonoid M] [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)

instance Prod.instAddCommMonoid {M : Type u_5} {N : Type u_6} [AddCommMonoid M] [AddCommMonoid N] : AddCommMonoid (M × N)

Equations

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

theorem Prod.instAddCommMonoid.proof_1 {M : Type u_1} {N : Type u_2} [AddCommMonoid M] [AddCommMonoid N] : ∀ (x x_1 : M × N), x + x_1 = x_1 + x

instance Prod.instCommMonoid {M : Type u_5} {N : Type u_6} [CommMonoid M] [CommMonoid N] : CommMonoid (M × N)

Equations

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

theorem Prod.instAddCancelCommMonoidSum.proof_1 {M : Type u_1} {N : Type u_2} [AddCancelCommMonoid M] [AddCancelCommMonoid N] : ∀ (x x_1 : M × N), x + x_1 = x_1 + x

instance Prod.instAddCancelCommMonoidSum {M : Type u_5} {N : Type u_6} [AddCancelCommMonoid M] [AddCancelCommMonoid N] : AddCancelCommMonoid (M × N)

Equations

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

instance Prod.instCancelCommMonoidProd {M : Type u_5} {N : Type u_6} [CancelCommMonoid M] [CancelCommMonoid N] : CancelCommMonoid (M × N)

Equations

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

instance Prod.instMulZeroOneClassProd {M : Type u_5} {N : Type u_6} [MulZeroOneClass M] [MulZeroOneClass N] : MulZeroOneClass (M × N)

Equations

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

instance Prod.instMonoidWithZeroProd {M : Type u_5} {N : Type u_6} [MonoidWithZero M] [MonoidWithZero N] : MonoidWithZero (M × N)

Equations

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

instance Prod.instCommMonoidWithZeroProd {M : Type u_5} {N : Type u_6} [CommMonoidWithZero M] [CommMonoidWithZero N] : CommMonoidWithZero (M × N)

Equations

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

theorem Prod.instAddCommGroup.proof_1 {G : Type u_1} {H : Type u_2} [AddCommGroup G] [AddCommGroup H] : ∀ (x x_1 : G × H), x + x_1 = x_1 + x

instance Prod.instAddCommGroup {G : Type u_3} {H : Type u_4} [AddCommGroup G] [AddCommGroup H] : AddCommGroup (G × H)

Equations

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

instance Prod.instCommGroup {G : Type u_3} {H : Type u_4} [CommGroup G] [CommGroup H] : CommGroup (G × H)

Equations

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

theorem AddSemiconjBy.prod {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} {z : M × N} (hm : AddSemiconjBy x.1 y.1 z.1) (hn : AddSemiconjBy x.2 y.2 z.2) : AddSemiconjBy x y z

theorem SemiconjBy.prod {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} (hm : SemiconjBy x.1 y.1 z.1) (hn : SemiconjBy x.2 y.2 z.2) : SemiconjBy x y z

theorem Prod.semiconjBy_iff {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} {z : M × N} : SemiconjBy x y z ↔ SemiconjBy x.1 y.1 z.1 ∧ SemiconjBy x.2 y.2 z.2

theorem AddCommute.prod {M : Type u_5} {N : Type u_6} [Add M] [Add N] {x : M × N} {y : M × N} (hm : AddCommute x.1 y.1) (hn : AddCommute x.2 y.2) : AddCommute x y

theorem Commute.prod {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} (hm : Commute x.1 y.1) (hn : Commute x.2 y.2) : Commute x y

theorem Prod.commute_iff {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] {x : M × N} {y : M × N} : Commute x y ↔ Commute x.1 y.1 ∧ Commute x.2 y.2

theorem AddHom.fst.proof_1 (M : Type u_1) (N : Type u_2) [Add M] [Add N] : ∀ (x x_1 : M × N), (x + x_1).1 = (x + x_1).1

def AddHom.fst (M : Type u_5) (N : Type u_6) [Add M] [Add N] : AddHom (M × N) M

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

Equations

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

def MulHom.fst (M : Type u_5) (N : Type u_6) [Mul M] [Mul N] : M × N →ₙ* M

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

Equations

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

theorem AddHom.snd.proof_1 (M : Type u_1) (N : Type u_2) [Add M] [Add N] : ∀ (x x_1 : M × N), (x + x_1).2 = (x + x_1).2

def AddHom.snd (M : Type u_5) (N : Type u_6) [Add M] [Add N] : AddHom (M × N) N

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

Equations

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

def MulHom.snd (M : Type u_5) (N : Type u_6) [Mul M] [Mul N] : M × N →ₙ* N

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

Equations

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

@[simp]

theorem AddHom.coe_fst {M : Type u_5} {N : Type u_6} [Add M] [Add N] : ⇑(AddHom.fst M N) = Prod.fst

@[simp]

theorem MulHom.coe_fst {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] : ⇑(MulHom.fst M N) = Prod.fst

@[simp]

theorem AddHom.coe_snd {M : Type u_5} {N : Type u_6} [Add M] [Add N] : ⇑(AddHom.snd M N) = Prod.snd

@[simp]

theorem MulHom.coe_snd {M : Type u_5} {N : Type u_6} [Mul M] [Mul N] : ⇑(MulHom.snd M N) = Prod.snd

theorem AddHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [Add M] [Add N] [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

def AddHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [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) 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) }

def MulHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : M →ₙ* N × P

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

Equations

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

theorem AddHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [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_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(MulHom.prod f g) = Pi.prod ⇑f ⇑g

@[simp]

theorem AddHom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [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_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [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_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) : AddHom.comp (AddHom.fst N P) (AddHom.prod f g) = f

@[simp]

theorem MulHom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : MulHom.comp (MulHom.fst N P) (MulHom.prod f g) = f

@[simp]

theorem AddHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [Add P] (f : AddHom M N) (g : AddHom M P) : AddHom.comp (AddHom.snd N P) (AddHom.prod f g) = g

@[simp]

theorem MulHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N) (g : M →ₙ* P) : MulHom.comp (MulHom.snd N P) (MulHom.prod f g) = g

@[simp]

theorem AddHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [Add P] (f : AddHom M (N × P)) : AddHom.prod (AddHom.comp (AddHom.fst N P) f) (AddHom.comp (AddHom.snd N P) f) = f

@[simp]

theorem MulHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [Mul P] (f : M →ₙ* N × P) : MulHom.prod (MulHom.comp (MulHom.fst N P) f) (MulHom.comp (MulHom.snd N P) f) = f

def AddHom.prodMap {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Add M] [Add N] [Add M'] [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))

def MulHom.prodMap {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [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))

theorem AddHom.prodMap_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Add M] [Add N] [Add M'] [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))

theorem MulHom.prodMap_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [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))

@[simp]

theorem AddHom.coe_prodMap {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Add M] [Add N] [Add M'] [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_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] (f : M →ₙ* M') (g : N →ₙ* N') : ⇑(MulHom.prodMap f g) = Prod.map ⇑f ⇑g

theorem AddHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [Add M] [Add N] [Add M'] [Add N'] [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)

theorem MulHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [Mul M] [Mul N] [Mul M'] [Mul N'] [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)

def AddHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [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. (Commutative codomain; for the general case, see AddHom.noncommCoprod)

Equations

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

def MulHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) : M × N →ₙ* P

Coproduct of two MulHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative codomain; for the general case, see MulHom.noncommCoprod)

Equations

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

@[simp]

theorem AddHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [AddCommSemigroup P] (f : AddHom M P) (g : AddHom N P) (p : M × N) : (AddHom.coprod f g) p = f p.1 + g p.2

@[simp]

theorem MulHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [CommSemigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) : (MulHom.coprod f g) p = f p.1 * g p.2

theorem AddHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Add M] [Add N] [AddCommSemigroup P] {Q : Type u_8} [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)

theorem MulHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [Mul M] [Mul N] [CommSemigroup P] {Q : Type u_8} [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)

theorem AddMonoidHom.fst.proof_2 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] : ∀ (x x_1 : M × N), { toFun := Prod.fst, map_zero' := (_ : 0.1 = 0.1) }.toFun (x + x_1) = { toFun := Prod.fst, map_zero' := (_ : 0.1 = 0.1) }.toFun (x + x_1)

theorem AddMonoidHom.fst.proof_1 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] : 0.1 = 0.1

def AddMonoidHom.fst (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] : M × N →+ M

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

Equations

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

def MonoidHom.fst (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] : M × N →* M

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

Equations

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

def AddMonoidHom.snd (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] : M × N →+ N

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

Equations

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

theorem AddMonoidHom.snd.proof_1 (M : Type u_2) (N : Type u_1) [AddZeroClass M] [AddZeroClass N] : 0.2 = 0.2

theorem AddMonoidHom.snd.proof_2 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] : ∀ (x x_1 : M × N), { toFun := Prod.snd, map_zero' := (_ : 0.2 = 0.2) }.toFun (x + x_1) = { toFun := Prod.snd, map_zero' := (_ : 0.2 = 0.2) }.toFun (x + x_1)

def MonoidHom.snd (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] : M × N →* N

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

Equations

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

def AddMonoidHom.inl (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] : M →+ M × N

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

Equations

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

theorem AddMonoidHom.inl.proof_1 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] : (fun (x : M) => (x, 0)) 0 = (fun (x : M) => (x, 0)) 0

theorem AddMonoidHom.inl.proof_2 (M : Type u_2) (N : Type u_1) [AddZeroClass M] [AddZeroClass N] : ∀ (x x_1 : M), { toFun := fun (x : M) => (x, 0), map_zero' := (_ : (fun (x : M) => (x, 0)) 0 = (fun (x : M) => (x, 0)) 0) }.toFun (x + x_1) = { toFun := fun (x : M) => (x, 0), map_zero' := (_ : (fun (x : M) => (x, 0)) 0 = (fun (x : M) => (x, 0)) 0) }.toFun x + { toFun := fun (x : M) => (x, 0), map_zero' := (_ : (fun (x : M) => (x, 0)) 0 = (fun (x : M) => (x, 0)) 0) }.toFun x_1

def MonoidHom.inl (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] : M →* M × N

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

Equations

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

theorem AddMonoidHom.inr.proof_1 (M : Type u_1) (N : Type u_2) [AddZeroClass M] [AddZeroClass N] : (fun (y : N) => (0, y)) 0 = (fun (y : N) => (0, y)) 0

def AddMonoidHom.inr (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] : N →+ M × N

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

Equations

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

theorem AddMonoidHom.inr.proof_2 (M : Type u_2) (N : Type u_1) [AddZeroClass M] [AddZeroClass N] : ∀ (x x_1 : N), { toFun := fun (y : N) => (0, y), map_zero' := (_ : (fun (y : N) => (0, y)) 0 = (fun (y : N) => (0, y)) 0) }.toFun (x + x_1) = { toFun := fun (y : N) => (0, y), map_zero' := (_ : (fun (y : N) => (0, y)) 0 = (fun (y : N) => (0, y)) 0) }.toFun x + { toFun := fun (y : N) => (0, y), map_zero' := (_ : (fun (y : N) => (0, y)) 0 = (fun (y : N) => (0, y)) 0) }.toFun x_1

def MonoidHom.inr (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] : N →* M × N

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

Equations

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

@[simp]

theorem AddMonoidHom.coe_fst {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : ⇑(AddMonoidHom.fst M N) = Prod.fst

@[simp]

theorem MonoidHom.coe_fst {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : ⇑(MonoidHom.fst M N) = Prod.fst

@[simp]

theorem AddMonoidHom.coe_snd {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : ⇑(AddMonoidHom.snd M N) = Prod.snd

@[simp]

theorem MonoidHom.coe_snd {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : ⇑(MonoidHom.snd M N) = Prod.snd

@[simp]

theorem AddMonoidHom.inl_apply {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] (x : M) : (AddMonoidHom.inl M N) x = (x, 0)

@[simp]

theorem MonoidHom.inl_apply {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] (x : M) : (MonoidHom.inl M N) x = (x, 1)

@[simp]

theorem AddMonoidHom.inr_apply {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] (y : N) : (AddMonoidHom.inr M N) y = (0, y)

@[simp]

theorem MonoidHom.inr_apply {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] (y : N) : (MonoidHom.inr M N) y = (1, y)

@[simp]

theorem AddMonoidHom.fst_comp_inl {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.comp (AddMonoidHom.fst M N) (AddMonoidHom.inl M N) = AddMonoidHom.id M

@[simp]

theorem MonoidHom.fst_comp_inl {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.inl M N) = MonoidHom.id M

@[simp]

theorem AddMonoidHom.snd_comp_inl {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.comp (AddMonoidHom.snd M N) (AddMonoidHom.inl M N) = 0

@[simp]

theorem MonoidHom.snd_comp_inl {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.inl M N) = 1

@[simp]

theorem AddMonoidHom.fst_comp_inr {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.comp (AddMonoidHom.fst M N) (AddMonoidHom.inr M N) = 0

@[simp]

theorem MonoidHom.fst_comp_inr {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : MonoidHom.comp (MonoidHom.fst M N) (MonoidHom.inr M N) = 1

@[simp]

theorem AddMonoidHom.snd_comp_inr {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.comp (AddMonoidHom.snd M N) (AddMonoidHom.inr M N) = AddMonoidHom.id N

@[simp]

theorem MonoidHom.snd_comp_inr {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : MonoidHom.comp (MonoidHom.snd M N) (MonoidHom.inr M N) = MonoidHom.id N

theorem AddMonoidHom.addCommute_inl_inr {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] (m : M) (n : N) : AddCommute ((AddMonoidHom.inl M N) m) ((AddMonoidHom.inr M N) n)

theorem MonoidHom.commute_inl_inr {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] (m : M) (n : N) : Commute ((MonoidHom.inl M N) m) ((MonoidHom.inr M N) n)

theorem AddMonoidHom.prod.proof_2 {M : Type u_3} {N : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) (x : M) (y : M) : { toFun := Pi.prod ⇑f ⇑g, map_zero' := (_ : Pi.prod (⇑f) (⇑g) 0 = 0) }.toFun (x + y) = { toFun := Pi.prod ⇑f ⇑g, map_zero' := (_ : Pi.prod (⇑f) (⇑g) 0 = 0) }.toFun x + { toFun := Pi.prod ⇑f ⇑g, map_zero' := (_ : Pi.prod (⇑f) (⇑g) 0 = 0) }.toFun y

theorem AddMonoidHom.prod.proof_1 {M : Type u_3} {N : Type u_2} {P : Type u_1} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : Pi.prod (⇑f) (⇑g) 0 = 0

def AddMonoidHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : M →+ N × P

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

Equations

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

def MonoidHom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : M →* N × P

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

Equations

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

theorem AddMonoidHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : ⇑(AddMonoidHom.prod f g) = Pi.prod ⇑f ⇑g

theorem MonoidHom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : ⇑(MonoidHom.prod f g) = Pi.prod ⇑f ⇑g

@[simp]

theorem AddMonoidHom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [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_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [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_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : AddMonoidHom.comp (AddMonoidHom.fst N P) (AddMonoidHom.prod f g) = f

@[simp]

theorem MonoidHom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : MonoidHom.comp (MonoidHom.fst N P) (MonoidHom.prod f g) = f

@[simp]

theorem AddMonoidHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N) (g : M →+ P) : AddMonoidHom.comp (AddMonoidHom.snd N P) (AddMonoidHom.prod f g) = g

@[simp]

theorem MonoidHom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N) (g : M →* P) : MonoidHom.comp (MonoidHom.snd N P) (MonoidHom.prod f g) = g

@[simp]

theorem AddMonoidHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (f : M →+ N × P) : AddMonoidHom.prod (AddMonoidHom.comp (AddMonoidHom.fst N P) f) (AddMonoidHom.comp (AddMonoidHom.snd N P) f) = f

@[simp]

theorem MonoidHom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [MulOneClass P] (f : M →* N × P) : MonoidHom.prod (MonoidHom.comp (MonoidHom.fst N P) f) (MonoidHom.comp (MonoidHom.snd N P) f) = f

def AddMonoidHom.prodMap {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] {M' : Type u_8} {N' : Type u_9} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : M × N →+ M' × N'

prod.map as an AddMonoidHom.

Equations

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

def MonoidHom.prodMap {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] {M' : Type u_8} {N' : Type u_9} [MulOneClass M'] [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))

theorem AddMonoidHom.prodMap_def {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] {M' : Type u_8} {N' : Type u_9} [AddZeroClass M'] [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))

theorem MonoidHom.prodMap_def {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] {M' : Type u_8} {N' : Type u_9} [MulOneClass M'] [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))

@[simp]

theorem AddMonoidHom.coe_prodMap {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] {M' : Type u_8} {N' : Type u_9} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ M') (g : N →+ N') : ⇑(AddMonoidHom.prodMap f g) = Prod.map ⇑f ⇑g

@[simp]

theorem MonoidHom.coe_prodMap {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] {M' : Type u_8} {N' : Type u_9} [MulOneClass M'] [MulOneClass N'] (f : M →* M') (g : N →* N') : ⇑(MonoidHom.prodMap f g) = Prod.map ⇑f ⇑g

theorem AddMonoidHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] {M' : Type u_8} {N' : Type u_9} [AddZeroClass M'] [AddZeroClass N'] [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)

theorem MonoidHom.prod_comp_prodMap {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] {M' : Type u_8} {N' : Type u_9} [MulOneClass M'] [MulOneClass N'] [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)

def AddMonoidHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) : M × N →+ P

Coproduct of two AddMonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 + g p.2. (Commutative case; for the general case, see AddHom.noncommCoprod.)

Equations

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

def MonoidHom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) : M × N →* P

Coproduct of two MonoidHoms with the same codomain: f.coprod g (p : M × N) = f p.1 * g p.2. (Commutative case; for the general case, see MonoidHom.noncommCoprod.)

Equations

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

@[simp]

theorem AddMonoidHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) (p : M × N) : (AddMonoidHom.coprod f g) p = f p.1 + g p.2

@[simp]

theorem MonoidHom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) (p : M × N) : (MonoidHom.coprod f g) p = f p.1 * g p.2

@[simp]

theorem AddMonoidHom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) : AddMonoidHom.comp (AddMonoidHom.coprod f g) (AddMonoidHom.inl M N) = f

@[simp]

theorem MonoidHom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) : MonoidHom.comp (MonoidHom.coprod f g) (MonoidHom.inl M N) = f

@[simp]

theorem AddMonoidHom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M →+ P) (g : N →+ P) : AddMonoidHom.comp (AddMonoidHom.coprod f g) (AddMonoidHom.inr M N) = g

@[simp]

theorem MonoidHom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M →* P) (g : N →* P) : MonoidHom.comp (MonoidHom.coprod f g) (MonoidHom.inr M N) = g

@[simp]

theorem AddMonoidHom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] (f : M × N →+ P) : AddMonoidHom.coprod (AddMonoidHom.comp f (AddMonoidHom.inl M N)) (AddMonoidHom.comp f (AddMonoidHom.inr M N)) = f

@[simp]

theorem MonoidHom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] (f : M × N →* P) : MonoidHom.coprod (MonoidHom.comp f (MonoidHom.inl M N)) (MonoidHom.comp f (MonoidHom.inr M N)) = f

@[simp]

theorem AddMonoidHom.coprod_inl_inr {M : Type u_8} {N : Type u_9} [AddCommMonoid M] [AddCommMonoid N] : AddMonoidHom.coprod (AddMonoidHom.inl M N) (AddMonoidHom.inr M N) = AddMonoidHom.id (M × N)

@[simp]

theorem MonoidHom.coprod_inl_inr {M : Type u_8} {N : Type u_9} [CommMonoid M] [CommMonoid N] : MonoidHom.coprod (MonoidHom.inl M N) (MonoidHom.inr M N) = MonoidHom.id (M × N)

theorem AddMonoidHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [AddZeroClass M] [AddZeroClass N] [AddCommMonoid P] {Q : Type u_8} [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)

theorem MonoidHom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [MulOneClass M] [MulOneClass N] [CommMonoid P] {Q : Type u_8} [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)

def AddEquiv.prodComm {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : M × N ≃+ N × M

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

Equations

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

theorem AddEquiv.prodComm.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : ∀ (x x_1 : M × N), (Equiv.prodComm M N).toFun (x + x_1) = (Equiv.prodComm M N).toFun x + (Equiv.prodComm M N).toFun x_1

def MulEquiv.prodComm {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : M × N ≃* N × M

The equivalence between M × N and N × 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_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : ⇑AddEquiv.prodComm = Prod.swap

@[simp]

theorem MulEquiv.coe_prodComm {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : ⇑MulEquiv.prodComm = Prod.swap

@[simp]

theorem AddEquiv.coe_prodComm_symm {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] : ⇑(AddEquiv.symm AddEquiv.prodComm) = Prod.swap

@[simp]

theorem MulEquiv.coe_prodComm_symm {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] : ⇑(MulEquiv.symm MulEquiv.prodComm) = Prod.swap

theorem AddEquiv.prodProdProdComm.proof_2 (M : Type u_1) (N : Type u_2) (M' : Type u_3) (N' : Type u_4) : Function.RightInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun

def AddEquiv.prodProdProdComm (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] (M' : Type u_8) (N' : Type u_9) [AddZeroClass M'] [AddZeroClass N'] : (M × N) × M' × N' ≃+ (M × M') × N × N'

Four-way commutativity of prod. The name matches mul_mul_mul_comm

Equations

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

theorem AddEquiv.prodProdProdComm.proof_1 (M : Type u_1) (N : Type u_2) (M' : Type u_3) (N' : Type u_4) : Function.LeftInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun

theorem AddEquiv.prodProdProdComm.proof_3 (M : Type u_2) (N : Type u_1) [AddZeroClass M] [AddZeroClass N] (M' : Type u_4) (N' : Type u_3) [AddZeroClass M'] [AddZeroClass N'] (_mnmn : (M × N) × M' × N') (_mnmn' : (M × N) × M' × N') : { toFun := fun (mnmn : (M × N) × M' × N') => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2), invFun := fun (mmnn : (M × M') × N × N') => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := (_ : Function.LeftInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun), right_inv := (_ : Function.RightInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun) }.toFun (_mnmn + _mnmn') = { toFun := fun (mnmn : (M × N) × M' × N') => ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2), invFun := fun (mmnn : (M × M') × N × N') => ((mmnn.1.1, mmnn.2.1), mmnn.1.2, mmnn.2.2), left_inv := (_ : Function.LeftInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun), right_inv := (_ : Function.RightInverse (Equiv.prodProdProdComm M N M' N').invFun (Equiv.prodProdProdComm M N M' N').toFun) }.toFun (_mnmn + _mnmn')

@[simp]

theorem MulEquiv.prodProdProdComm_apply (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] (M' : Type u_8) (N' : Type u_9) [MulOneClass M'] [MulOneClass N'] (mnmn : (M × N) × M' × N') : (MulEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

@[simp]

theorem AddEquiv.prodProdProdComm_apply (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] (M' : Type u_8) (N' : Type u_9) [AddZeroClass M'] [AddZeroClass N'] (mnmn : (M × N) × M' × N') : (AddEquiv.prodProdProdComm M N M' N') mnmn = ((mnmn.1.1, mnmn.2.1), mnmn.1.2, mnmn.2.2)

def MulEquiv.prodProdProdComm (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] (M' : Type u_8) (N' : Type u_9) [MulOneClass M'] [MulOneClass N'] : (M × N) × M' × N' ≃* (M × M') × N × N'

Four-way commutativity of prod. The name matches mul_mul_mul_comm.

Equations

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

@[simp]

theorem AddEquiv.prodProdProdComm_toEquiv (M : Type u_5) (N : Type u_6) [AddZeroClass M] [AddZeroClass N] (M' : Type u_8) (N' : Type u_9) [AddZeroClass M'] [AddZeroClass N'] : ↑(AddEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

@[simp]

theorem MulEquiv.prodProdProdComm_toEquiv (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] (M' : Type u_8) (N' : Type u_9) [MulOneClass M'] [MulOneClass N'] : ↑(MulEquiv.prodProdProdComm M N M' N') = Equiv.prodProdProdComm M N M' N'

@[simp]

theorem MulEquiv.prodProdProdComm_symm (M : Type u_5) (N : Type u_6) [MulOneClass M] [MulOneClass N] (M' : Type u_8) (N' : Type u_9) [MulOneClass M'] [MulOneClass N'] : MulEquiv.symm (MulEquiv.prodProdProdComm M N M' N') = MulEquiv.prodProdProdComm M M' N N'

def AddEquiv.prodCongr {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] {M' : Type u_8} {N' : Type u_9} [AddZeroClass M'] [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.

theorem AddEquiv.prodCongr.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_4} {N' : Type u_3} [AddZeroClass M'] [AddZeroClass N'] (f : M ≃+ M') (g : N ≃+ N') : ∀ (x x_1 : M × N), (Equiv.prodCongr f.toEquiv g.toEquiv).toFun (x + x_1) = (Equiv.prodCongr f.toEquiv g.toEquiv).toFun x + (Equiv.prodCongr f.toEquiv g.toEquiv).toFun x_1

def MulEquiv.prodCongr {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] {M' : Type u_8} {N' : Type u_9} [MulOneClass M'] [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.

theorem AddEquiv.uniqueProd.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] [Unique N] : ∀ (x x_1 : N × M), (Equiv.uniqueProd M N).toFun (x + x_1) = (Equiv.uniqueProd M N).toFun (x + x_1)

def AddEquiv.uniqueProd {M : Type u_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] [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 MulEquiv.uniqueProd {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] [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_5} {N : Type u_6} [AddZeroClass M] [AddZeroClass N] [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.

theorem AddEquiv.prodUnique.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] [Unique N] : ∀ (x x_1 : M × N), (Equiv.prodUnique M N).toFun (x + x_1) = (Equiv.prodUnique M N).toFun (x + x_1)

def MulEquiv.prodUnique {M : Type u_5} {N : Type u_6} [MulOneClass M] [MulOneClass N] [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.

theorem AddEquiv.prodAddUnits.proof_4 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] : ∀ (x : AddUnits M × AddUnits N), (AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) ((fun (u : AddUnits M × AddUnits N) => { val := (↑u.1, ↑u.2), neg := (↑(-u.1), ↑(-u.2)), val_neg := (_ : (↑u.1 + ↑(-u.1), ↑u.2 + ↑(-u.2)) = 0), neg_val := (_ : (↑(-u.1) + ↑u.1, ↑(-u.2) + ↑u.2) = 0) }) x) = x

def AddEquiv.prodAddUnits {M : Type u_5} {N : Type u_6} [AddMonoid M] [AddMonoid N] : AddUnits (M × N) ≃+ AddUnits M × AddUnits N

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

Equations

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

theorem AddEquiv.prodAddUnits.proof_3 {M : Type u_2} {N : Type u_1} [AddMonoid M] [AddMonoid N] (u : AddUnits (M × N)) : { val := (↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1, ↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2), neg := (↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1), ↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2)), val_neg := (_ : (↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1 + ↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1), ↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2 + ↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2)) = 0), neg_val := (_ : (↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1) + ↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).1, ↑(-((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2) + ↑((AddMonoidHom.prod (AddUnits.map (AddMonoidHom.fst M N)) (AddUnits.map (AddMonoidHom.snd M N))) u).2) = 0) } = u

theorem AddEquiv.prodAddUnits.proof_5 {M : Type u_2} {N : Type u_1} [AddMonoid M] [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

abbrev AddEquiv.prodAddUnits.match_1 {M : Type u_1} {N : Type u_2} [AddMonoid M] [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

• (_ : motive x) = (_ : motive x)

theorem AddEquiv.prodAddUnits.proof_1 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (u : AddUnits M × AddUnits N) : (↑u.1 + ↑(-u.1), ↑u.2 + ↑(-u.2)) = 0

theorem AddEquiv.prodAddUnits.proof_2 {M : Type u_1} {N : Type u_2} [AddMonoid M] [AddMonoid N] (u : AddUnits M × AddUnits N) : (↑(-u.1) + ↑u.1, ↑(-u.2) + ↑u.2) = 0

def MulEquiv.prodUnits {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] : (M × N)ˣ ≃* Mˣ × Nˣ

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

Equations

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

theorem AddUnits.embedProduct.proof_2 (α : Type u_1) [AddMonoid α] (x : AddUnits α) (y : AddUnits α) : (↑x + ↑y, AddOpposite.op ↑(-(x + y))) = (↑x + ↑y, AddOpposite.op ↑(-x) + AddOpposite.op ↑(-y))

theorem AddUnits.embedProduct.proof_1 (α : Type u_1) [AddMonoid α] : (0, AddOpposite.op ↑(-0)) = 0

def AddUnits.embedProduct (α : Type u_8) [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.

@[simp]

theorem Units.embedProduct_apply (α : Type u_8) [Monoid α] (x : αˣ) : (Units.embedProduct α) x = (↑x, MulOpposite.op ↑x⁻¹)

@[simp]

theorem AddUnits.embedProduct_apply (α : Type u_8) [AddMonoid α] (x : AddUnits α) : (AddUnits.embedProduct α) x = (↑x, AddOpposite.op ↑(-x))

def Units.embedProduct (α : Type u_8) [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.

theorem AddUnits.embedProduct_injective (α : Type u_8) [AddMonoid α] : Function.Injective ⇑(AddUnits.embedProduct α)

theorem Units.embedProduct_injective (α : Type u_8) [Monoid α] : Function.Injective ⇑(Units.embedProduct α)

Multiplication and division as homomorphisms

theorem addAddHom.proof_1 {α : Type u_1} [AddCommSemigroup α] : ∀ (x x_1 : α × α), x.1 + x_1.1 + (x.2 + x_1.2) = x.1 + x.2 + (x_1.1 + x_1.2)

def addAddHom {α : Type u_8} [AddCommSemigroup α] : AddHom (α × α) α

Addition as an additive homomorphism.

Equations

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

@[simp]

theorem mulMulHom_apply {α : Type u_8} [CommSemigroup α] (a : α × α) : mulMulHom a = a.1 * a.2

@[simp]

theorem addAddHom_apply {α : Type u_8} [AddCommSemigroup α] (a : α × α) : addAddHom a = a.1 + a.2

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

Multiplication as a multiplicative homomorphism.

Equations

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

theorem addAddMonoidHom.proof_1 {α : Type u_1} [AddCommMonoid α] : 0.1 + 0 = 0.1

def addAddMonoidHom {α : Type u_8} [AddCommMonoid α] : α × α →+ α

Addition as an additive monoid homomorphism.

Equations

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

theorem addAddMonoidHom.proof_2 {α : Type u_1} [AddCommMonoid α] (x : α × α) (y : α × α) : addAddHom.toFun (x + y) = addAddHom.toFun x + addAddHom.toFun y

@[simp]

theorem addAddMonoidHom_apply {α : Type u_8} [AddCommMonoid α] : ∀ (a : α × α), addAddMonoidHom a = addAddHom.toFun a

@[simp]

theorem mulMonoidHom_apply {α : Type u_8} [CommMonoid α] : ∀ (a : α × α), mulMonoidHom a = mulMulHom.toFun a

def mulMonoidHom {α : Type u_8} [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_8} [CommMonoidWithZero α] : ∀ (a : α × α), mulMonoidWithZeroHom a = (↑mulMonoidHom).toFun a

def mulMonoidWithZeroHom {α : Type u_8} [CommMonoidWithZero α] : α × α →*₀ α

Multiplication as a multiplicative homomorphism with zero.

Equations

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

theorem subAddMonoidHom.proof_2 {α : Type u_1} [SubtractionCommMonoid α] : ∀ (x x_1 : α × α), x.1 + x_1.1 - (x.2 + x_1.2) = x.1 - x.2 + (x_1.1 - x_1.2)

def subAddMonoidHom {α : Type u_8} [SubtractionCommMonoid α] : α × α →+ α

Subtraction as an additive monoid homomorphism.

Equations

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

theorem subAddMonoidHom.proof_1 {α : Type u_1} [SubtractionCommMonoid α] : 0.1 - 0 = 0.1

@[simp]

theorem divMonoidHom_apply {α : Type u_8} [DivisionCommMonoid α] (a : α × α) : divMonoidHom a = a.1 / a.2

@[simp]

theorem subAddMonoidHom_apply {α : Type u_8} [SubtractionCommMonoid α] (a : α × α) : subAddMonoidHom a = a.1 - a.2

def divMonoidHom {α : Type u_8} [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_8} [CommGroupWithZero α] (a : α × α) : divMonoidWithZeroHom a = a.1 / a.2

def divMonoidWithZeroHom {α : Type u_8} [CommGroupWithZero α] : α × α →*₀ α

Division as a multiplicative homomorphism with zero.

Equations

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