algebra.group.prod - mathlib3 docs

source

@[protected, instance]

def prod.has_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :

has_mul (M × N)

Equations

prod.has_mul = {mul := λ (p q : M × N), (p.fst * q.fst, p.snd * q.snd)}

source

@[protected, instance]

def prod.has_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :

has_add (M × N)

Equations

prod.has_add = {add := λ (p q : M × N), (p.fst + q.fst, p.snd + q.snd)}

source

@[simp]

theorem prod.fst_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :

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

source

@[simp]

theorem prod.fst_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :

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

source

@[simp]

theorem prod.snd_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :

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

source

@[simp]

theorem prod.snd_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :

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

source

@[simp]

theorem prod.mk_add_mk {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (a₁ a₂ : M) (b₁ b₂ : N) :

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

source

@[simp]

theorem prod.mk_mul_mk {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (a₁ a₂ : M) (b₁ b₂ : N) :

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

source

@[simp]

theorem prod.swap_mul {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :

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

source

@[simp]

theorem prod.swap_add {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :

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

source

theorem prod.mul_def {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] (p q : M × N) :

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

source

theorem prod.add_def {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] (p q : M × N) :

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

source

theorem prod.zero_mk_add_zero_mk {M : Type u_5} {N : Type u_6} [add_monoid M] [has_add N] (b₁ b₂ : N) :

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

source

theorem prod.one_mk_mul_one_mk {M : Type u_5} {N : Type u_6} [monoid M] [has_mul N] (b₁ b₂ : N) :

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

source

theorem prod.mk_zero_add_mk_zero {M : Type u_5} {N : Type u_6} [has_add M] [add_monoid N] (a₁ a₂ : M) :

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

source

theorem prod.mk_one_mul_mk_one {M : Type u_5} {N : Type u_6} [has_mul M] [monoid N] (a₁ a₂ : M) :

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

source

@[protected, instance]

def prod.has_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :

has_one (M × N)

Equations

prod.has_one = {one := (1, 1)}

source

@[protected, instance]

def prod.has_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :

has_zero (M × N)

Equations

prod.has_zero = {zero := (0, 0)}

source

@[simp]

theorem prod.fst_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :

0.fst = 0

source

@[simp]

theorem prod.fst_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :

1.fst = 1

source

@[simp]

theorem prod.snd_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :

1.snd = 1

source

@[simp]

theorem prod.snd_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :

0.snd = 0

source

theorem prod.one_eq_mk {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :

1 = (1, 1)

source

theorem prod.zero_eq_mk {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :

0 = (0, 0)

source

@[simp]

theorem prod.mk_eq_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] {x : M} {y : N} :

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

source

@[simp]

theorem prod.mk_eq_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] {x : M} {y : N} :

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

source

@[simp]

theorem prod.swap_zero {M : Type u_5} {N : Type u_6} [has_zero M] [has_zero N] :

0.swap = 0

source

@[simp]

theorem prod.swap_one {M : Type u_5} {N : Type u_6} [has_one M] [has_one N] :

1.swap = 1

source

theorem prod.fst_mul_snd {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (p : M × N) :

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

source

theorem prod.fst_add_snd {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (p : M × N) :

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

source

@[protected, instance]

def prod.has_neg {M : Type u_5} {N : Type u_6} [has_neg M] [has_neg N] :

has_neg (M × N)

Equations

prod.has_neg = {neg := λ (p : M × N), (-p.fst, -p.snd)}

source

@[protected, instance]

def prod.has_inv {M : Type u_5} {N : Type u_6} [has_inv M] [has_inv N] :

has_inv (M × N)

Equations

prod.has_inv = {inv := λ (p : M × N), ((p.fst)⁻¹, (p.snd)⁻¹)}

source

@[simp]

theorem prod.fst_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :

(-p).fst = -p.fst

source

@[simp]

theorem prod.fst_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :

p⁻¹.fst = (p.fst)⁻¹

source

@[simp]

theorem prod.snd_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :

p⁻¹.snd = (p.snd)⁻¹

source

@[simp]

theorem prod.snd_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :

(-p).snd = -p.snd

source

@[simp]

theorem prod.inv_mk {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (a : G) (b : H) :

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

source

@[simp]

theorem prod.neg_mk {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (a : G) (b : H) :

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

source

@[simp]

theorem prod.swap_neg {G : Type u_3} {H : Type u_4} [has_neg G] [has_neg H] (p : G × H) :

(-p).swap = -p.swap

source

@[simp]

theorem prod.swap_inv {G : Type u_3} {H : Type u_4} [has_inv G] [has_inv H] (p : G × H) :

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

source

@[protected, instance]

def prod.has_involutive_inv {M : Type u_5} {N : Type u_6} [has_involutive_inv M] [has_involutive_inv N] :

has_involutive_inv (M × N)

Equations

prod.has_involutive_inv = {inv := has_inv.inv prod.has_inv, inv_inv := _}

source

@[protected, instance]

def prod.has_involutive_neg {M : Type u_5} {N : Type u_6} [has_involutive_neg M] [has_involutive_neg N] :

has_involutive_neg (M × N)

Equations

prod.has_involutive_neg = {neg := has_neg.neg prod.has_neg, neg_neg := _}

source

@[protected, instance]

def prod.has_div {M : Type u_5} {N : Type u_6} [has_div M] [has_div N] :

has_div (M × N)

Equations

prod.has_div = {div := λ (p q : M × N), (p.fst / q.fst, p.snd / q.snd)}

source

@[protected, instance]

def prod.has_sub {M : Type u_5} {N : Type u_6} [has_sub M] [has_sub N] :

has_sub (M × N)

Equations

prod.has_sub = {sub := λ (p q : M × N), (p.fst - q.fst, p.snd - q.snd)}

source

@[simp]

theorem prod.fst_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :

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

source

@[simp]

theorem prod.fst_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :

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

source

@[simp]

theorem prod.snd_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :

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

source

@[simp]

theorem prod.snd_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :

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

source

@[simp]

theorem prod.mk_sub_mk {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (x₁ x₂ : G) (y₁ y₂ : H) :

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

source

@[simp]

theorem prod.mk_div_mk {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (x₁ x₂ : G) (y₁ y₂ : H) :

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

source

@[simp]

theorem prod.swap_div {G : Type u_3} {H : Type u_4} [has_div G] [has_div H] (a b : G × H) :

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

source

@[simp]

theorem prod.swap_sub {G : Type u_3} {H : Type u_4} [has_sub G] [has_sub H] (a b : G × H) :

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

source

@[protected, instance]

def prod.mul_zero_class {M : Type u_5} {N : Type u_6} [mul_zero_class M] [mul_zero_class N] :

mul_zero_class (M × N)

Equations

prod.mul_zero_class = {mul := has_mul.mul prod.has_mul, zero := 0, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.semigroup {M : Type u_5} {N : Type u_6} [semigroup M] [semigroup N] :

semigroup (M × N)

Equations

prod.semigroup = {mul := has_mul.mul prod.has_mul, mul_assoc := _}

source

@[protected, instance]

def prod.add_semigroup {M : Type u_5} {N : Type u_6} [add_semigroup M] [add_semigroup N] :

add_semigroup (M × N)

Equations

prod.add_semigroup = {add := has_add.add prod.has_add, add_assoc := _}

source

@[protected, instance]

def prod.add_comm_semigroup {G : Type u_3} {H : Type u_4} [add_comm_semigroup G] [add_comm_semigroup H] :

add_comm_semigroup (G × H)

Equations

prod.add_comm_semigroup = {add := add_semigroup.add prod.add_semigroup, add_assoc := _, add_comm := _}

source

@[protected, instance]

def prod.comm_semigroup {G : Type u_3} {H : Type u_4} [comm_semigroup G] [comm_semigroup H] :

comm_semigroup (G × H)

Equations

prod.comm_semigroup = {mul := semigroup.mul prod.semigroup, mul_assoc := _, mul_comm := _}

source

@[protected, instance]

def prod.semigroup_with_zero {M : Type u_5} {N : Type u_6} [semigroup_with_zero M] [semigroup_with_zero N] :

semigroup_with_zero (M × N)

Equations

prod.semigroup_with_zero = {mul := mul_zero_class.mul prod.mul_zero_class, mul_assoc := _, zero := mul_zero_class.zero prod.mul_zero_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.add_zero_class {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

add_zero_class (M × N)

Equations

prod.add_zero_class = {zero := 0, add := has_add.add prod.has_add, zero_add := _, add_zero := _}

source

@[protected, instance]

def prod.mul_one_class {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

mul_one_class (M × N)

Equations

prod.mul_one_class = {one := 1, mul := has_mul.mul prod.has_mul, one_mul := _, mul_one := _}

source

@[protected, instance]

def prod.monoid {M : Type u_5} {N : Type u_6} [monoid M] [monoid N] :

monoid (M × N)

Equations

prod.monoid = {mul := semigroup.mul prod.semigroup, mul_assoc := _, one := mul_one_class.one prod.mul_one_class, one_mul := _, mul_one := _, npow := λ (z : ℕ) (a : M × N), (monoid.npow z a.fst, monoid.npow z a.snd), npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def prod.add_monoid {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] :

add_monoid (M × N)

Equations

prod.add_monoid = {add := add_semigroup.add prod.add_semigroup, add_assoc := _, zero := add_zero_class.zero prod.add_zero_class, zero_add := _, add_zero := _, nsmul := λ (z : ℕ) (a : M × N), (add_monoid.nsmul z a.fst, add_monoid.nsmul z a.snd), nsmul_zero' := _, nsmul_succ' := _}

source

@[protected, instance]

def prod.div_inv_monoid {G : Type u_3} {H : Type u_4} [div_inv_monoid G] [div_inv_monoid H] :

div_inv_monoid (G × H)

Equations

prod.div_inv_monoid = {mul := monoid.mul prod.monoid, mul_assoc := _, one := monoid.one prod.monoid, one_mul := _, mul_one := _, npow := monoid.npow prod.monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv prod.has_inv, div := has_div.div prod.has_div, div_eq_mul_inv := _, zpow := λ (z : ℤ) (a : G × H), (div_inv_monoid.zpow z a.fst, div_inv_monoid.zpow z a.snd), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _}

source

@[protected, instance]

def prod.sub_neg_monoid {G : Type u_3} {H : Type u_4} [sub_neg_monoid G] [sub_neg_monoid H] :

sub_neg_monoid (G × H)

Equations

prod.sub_neg_monoid = {add := add_monoid.add prod.add_monoid, add_assoc := _, zero := add_monoid.zero prod.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul prod.add_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg prod.has_neg, sub := has_sub.sub prod.has_sub, sub_eq_add_neg := _, zsmul := λ (z : ℤ) (a : G × H), (sub_neg_monoid.zsmul z a.fst, sub_neg_monoid.zsmul z a.snd), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _}

source

@[protected, instance]

def prod.division_monoid {G : Type u_3} {H : Type u_4} [division_monoid G] [division_monoid H] :

division_monoid (G × H)

Equations

prod.division_monoid = {mul := div_inv_monoid.mul prod.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one prod.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow prod.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv prod.div_inv_monoid, div := div_inv_monoid.div prod.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow prod.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _}

source

@[protected, instance]

def prod.subtraction_monoid {G : Type u_3} {H : Type u_4} [subtraction_monoid G] [subtraction_monoid H] :

subtraction_monoid (G × H)

Equations

prod.subtraction_monoid = {add := sub_neg_monoid.add prod.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero prod.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul prod.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg prod.sub_neg_monoid, sub := sub_neg_monoid.sub prod.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul prod.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _}

source

@[protected, instance]

def prod.subtraction_comm_monoid {G : Type u_3} {H : Type u_4} [subtraction_comm_monoid G] [subtraction_comm_monoid H] :

subtraction_comm_monoid (G × H)

Equations

prod.subtraction_comm_monoid = {add := subtraction_monoid.add prod.subtraction_monoid, add_assoc := _, zero := subtraction_monoid.zero prod.subtraction_monoid, zero_add := _, add_zero := _, nsmul := subtraction_monoid.nsmul prod.subtraction_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := subtraction_monoid.neg prod.subtraction_monoid, sub := subtraction_monoid.sub prod.subtraction_monoid, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul prod.subtraction_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}

source

@[protected, instance]

def prod.division_comm_monoid {G : Type u_3} {H : Type u_4} [division_comm_monoid G] [division_comm_monoid H] :

division_comm_monoid (G × H)

Equations

prod.division_comm_monoid = {mul := division_monoid.mul prod.division_monoid, mul_assoc := _, one := division_monoid.one prod.division_monoid, one_mul := _, mul_one := _, npow := division_monoid.npow prod.division_monoid, npow_zero' := _, npow_succ' := _, inv := division_monoid.inv prod.division_monoid, div := division_monoid.div prod.division_monoid, div_eq_mul_inv := _, zpow := division_monoid.zpow prod.division_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}

source

@[protected, instance]

def prod.add_group {G : Type u_3} {H : Type u_4} [add_group G] [add_group H] :

add_group (G × H)

Equations

prod.add_group = {add := sub_neg_monoid.add prod.sub_neg_monoid, add_assoc := _, zero := sub_neg_monoid.zero prod.sub_neg_monoid, zero_add := _, add_zero := _, nsmul := sub_neg_monoid.nsmul prod.sub_neg_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := sub_neg_monoid.neg prod.sub_neg_monoid, sub := sub_neg_monoid.sub prod.sub_neg_monoid, sub_eq_add_neg := _, zsmul := sub_neg_monoid.zsmul prod.sub_neg_monoid, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _}

source

@[protected, instance]

def prod.group {G : Type u_3} {H : Type u_4} [group G] [group H] :

group (G × H)

Equations

prod.group = {mul := div_inv_monoid.mul prod.div_inv_monoid, mul_assoc := _, one := div_inv_monoid.one prod.div_inv_monoid, one_mul := _, mul_one := _, npow := div_inv_monoid.npow prod.div_inv_monoid, npow_zero' := _, npow_succ' := _, inv := div_inv_monoid.inv prod.div_inv_monoid, div := div_inv_monoid.div prod.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow prod.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}

source

@[protected, instance]

def prod.left_cancel_add_semigroup {G : Type u_3} {H : Type u_4} [add_left_cancel_semigroup G] [add_left_cancel_semigroup H] :

add_left_cancel_semigroup (G × H)

Equations

prod.left_cancel_add_semigroup = {add := add_semigroup.add prod.add_semigroup, add_assoc := _, add_left_cancel := _}

source

@[protected, instance]

def prod.left_cancel_semigroup {G : Type u_3} {H : Type u_4} [left_cancel_semigroup G] [left_cancel_semigroup H] :

left_cancel_semigroup (G × H)

Equations

prod.left_cancel_semigroup = {mul := semigroup.mul prod.semigroup, mul_assoc := _, mul_left_cancel := _}

source

@[protected, instance]

def prod.right_cancel_add_semigroup {G : Type u_3} {H : Type u_4} [add_right_cancel_semigroup G] [add_right_cancel_semigroup H] :

add_right_cancel_semigroup (G × H)

Equations

prod.right_cancel_add_semigroup = {add := add_semigroup.add prod.add_semigroup, add_assoc := _, add_right_cancel := _}

source

@[protected, instance]

def prod.right_cancel_semigroup {G : Type u_3} {H : Type u_4} [right_cancel_semigroup G] [right_cancel_semigroup H] :

right_cancel_semigroup (G × H)

Equations

prod.right_cancel_semigroup = {mul := semigroup.mul prod.semigroup, mul_assoc := _, mul_right_cancel := _}

source

@[protected, instance]

def prod.left_cancel_monoid {M : Type u_5} {N : Type u_6} [left_cancel_monoid M] [left_cancel_monoid N] :

left_cancel_monoid (M × N)

Equations

prod.left_cancel_monoid = {mul := left_cancel_semigroup.mul prod.left_cancel_semigroup, mul_assoc := _, mul_left_cancel := _, one := monoid.one prod.monoid, one_mul := _, mul_one := _, npow := monoid.npow prod.monoid, npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def prod.left_cancel_add_monoid {M : Type u_5} {N : Type u_6} [add_left_cancel_monoid M] [add_left_cancel_monoid N] :

add_left_cancel_monoid (M × N)

Equations

prod.left_cancel_add_monoid = {add := add_left_cancel_semigroup.add prod.left_cancel_add_semigroup, add_assoc := _, add_left_cancel := _, zero := add_monoid.zero prod.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul prod.add_monoid, nsmul_zero' := _, nsmul_succ' := _}

source

@[protected, instance]

def prod.right_cancel_add_monoid {M : Type u_5} {N : Type u_6} [add_right_cancel_monoid M] [add_right_cancel_monoid N] :

add_right_cancel_monoid (M × N)

Equations

prod.right_cancel_add_monoid = {add := add_right_cancel_semigroup.add prod.right_cancel_add_semigroup, add_assoc := _, add_right_cancel := _, zero := add_monoid.zero prod.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul prod.add_monoid, nsmul_zero' := _, nsmul_succ' := _}

source

@[protected, instance]

def prod.right_cancel_monoid {M : Type u_5} {N : Type u_6} [right_cancel_monoid M] [right_cancel_monoid N] :

right_cancel_monoid (M × N)

Equations

prod.right_cancel_monoid = {mul := right_cancel_semigroup.mul prod.right_cancel_semigroup, mul_assoc := _, mul_right_cancel := _, one := monoid.one prod.monoid, one_mul := _, mul_one := _, npow := monoid.npow prod.monoid, npow_zero' := _, npow_succ' := _}

source

@[protected, instance]

def prod.cancel_add_monoid {M : Type u_5} {N : Type u_6} [add_cancel_monoid M] [add_cancel_monoid N] :

add_cancel_monoid (M × N)

Equations

prod.cancel_add_monoid = {add := add_right_cancel_monoid.add prod.right_cancel_add_monoid, add_assoc := _, add_left_cancel := _, zero := add_right_cancel_monoid.zero prod.right_cancel_add_monoid, zero_add := _, add_zero := _, nsmul := add_right_cancel_monoid.nsmul prod.right_cancel_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_right_cancel := _}

source

@[protected, instance]

def prod.cancel_monoid {M : Type u_5} {N : Type u_6} [cancel_monoid M] [cancel_monoid N] :

cancel_monoid (M × N)

Equations

prod.cancel_monoid = {mul := right_cancel_monoid.mul prod.right_cancel_monoid, mul_assoc := _, mul_left_cancel := _, one := right_cancel_monoid.one prod.right_cancel_monoid, one_mul := _, mul_one := _, npow := right_cancel_monoid.npow prod.right_cancel_monoid, npow_zero' := _, npow_succ' := _, mul_right_cancel := _}

source

@[protected, instance]

def prod.add_comm_monoid {M : Type u_5} {N : Type u_6} [add_comm_monoid M] [add_comm_monoid N] :

add_comm_monoid (M × N)

Equations

prod.add_comm_monoid = {add := add_comm_semigroup.add prod.add_comm_semigroup, add_assoc := _, zero := add_monoid.zero prod.add_monoid, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul prod.add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def prod.comm_monoid {M : Type u_5} {N : Type u_6} [comm_monoid M] [comm_monoid N] :

comm_monoid (M × N)

Equations

prod.comm_monoid = {mul := comm_semigroup.mul prod.comm_semigroup, mul_assoc := _, one := monoid.one prod.monoid, one_mul := _, mul_one := _, npow := monoid.npow prod.monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def prod.cancel_comm_monoid {M : Type u_5} {N : Type u_6} [cancel_comm_monoid M] [cancel_comm_monoid N] :

cancel_comm_monoid (M × N)

Equations

prod.cancel_comm_monoid = {mul := left_cancel_monoid.mul prod.left_cancel_monoid, mul_assoc := _, mul_left_cancel := _, one := left_cancel_monoid.one prod.left_cancel_monoid, one_mul := _, mul_one := _, npow := left_cancel_monoid.npow prod.left_cancel_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def prod.cancel_add_comm_monoid {M : Type u_5} {N : Type u_6} [add_cancel_comm_monoid M] [add_cancel_comm_monoid N] :

add_cancel_comm_monoid (M × N)

Equations

prod.cancel_add_comm_monoid = {add := add_left_cancel_monoid.add prod.left_cancel_add_monoid, add_assoc := _, add_left_cancel := _, zero := add_left_cancel_monoid.zero prod.left_cancel_add_monoid, zero_add := _, add_zero := _, nsmul := add_left_cancel_monoid.nsmul prod.left_cancel_add_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def prod.mul_zero_one_class {M : Type u_5} {N : Type u_6} [mul_zero_one_class M] [mul_zero_one_class N] :

mul_zero_one_class (M × N)

Equations

prod.mul_zero_one_class = {one := mul_one_class.one prod.mul_one_class, mul := mul_zero_class.mul prod.mul_zero_class, one_mul := _, mul_one := _, zero := mul_zero_class.zero prod.mul_zero_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.monoid_with_zero {M : Type u_5} {N : Type u_6} [monoid_with_zero M] [monoid_with_zero N] :

monoid_with_zero (M × N)

Equations

prod.monoid_with_zero = {mul := monoid.mul prod.monoid, mul_assoc := _, one := monoid.one prod.monoid, one_mul := _, mul_one := _, npow := monoid.npow prod.monoid, npow_zero' := _, npow_succ' := _, zero := mul_zero_one_class.zero prod.mul_zero_one_class, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.comm_monoid_with_zero {M : Type u_5} {N : Type u_6} [comm_monoid_with_zero M] [comm_monoid_with_zero N] :

comm_monoid_with_zero (M × N)

Equations

prod.comm_monoid_with_zero = {mul := comm_monoid.mul prod.comm_monoid, mul_assoc := _, one := comm_monoid.one prod.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow prod.comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := monoid_with_zero.zero prod.monoid_with_zero, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def prod.add_comm_group {G : Type u_3} {H : Type u_4} [add_comm_group G] [add_comm_group H] :

add_comm_group (G × H)

Equations

prod.add_comm_group = {add := add_comm_semigroup.add prod.add_comm_semigroup, add_assoc := _, zero := add_group.zero prod.add_group, zero_add := _, add_zero := _, nsmul := add_group.nsmul prod.add_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_group.neg prod.add_group, sub := add_group.sub prod.add_group, sub_eq_add_neg := _, zsmul := add_group.zsmul prod.add_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected, instance]

def prod.comm_group {G : Type u_3} {H : Type u_4} [comm_group G] [comm_group H] :

comm_group (G × H)

Equations

prod.comm_group = {mul := comm_semigroup.mul prod.comm_semigroup, mul_assoc := _, one := group.one prod.group, one_mul := _, mul_one := _, npow := group.npow prod.group, npow_zero' := _, npow_succ' := _, inv := group.inv prod.group, div := group.div prod.group, div_eq_mul_inv := _, zpow := group.zpow prod.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}

source

def mul_hom.fst (M : Type u_5) (N : Type u_6) [has_mul M] [has_mul N] :

M × N →ₙ* M

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

Equations

mul_hom.fst M N = {to_fun := prod.fst N, map_mul' := _}

source

def add_hom.fst (M : Type u_5) (N : Type u_6) [has_add M] [has_add N] :

add_hom (M × N) M

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

Equations

add_hom.fst M N = {to_fun := prod.fst N, map_add' := _}

source

def add_hom.snd (M : Type u_5) (N : Type u_6) [has_add M] [has_add N] :

add_hom (M × N) N

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

Equations

add_hom.snd M N = {to_fun := prod.snd N, map_add' := _}

source

def mul_hom.snd (M : Type u_5) (N : Type u_6) [has_mul M] [has_mul N] :

M × N →ₙ* N

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

Equations

mul_hom.snd M N = {to_fun := prod.snd N, map_mul' := _}

source

@[simp]

theorem mul_hom.coe_fst {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :

⇑(mul_hom.fst M N) = prod.fst

source

@[simp]

theorem add_hom.coe_fst {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :

⇑(add_hom.fst M N) = prod.fst

source

@[simp]

theorem mul_hom.coe_snd {M : Type u_5} {N : Type u_6} [has_mul M] [has_mul N] :

⇑(mul_hom.snd M N) = prod.snd

source

@[simp]

theorem add_hom.coe_snd {M : Type u_5} {N : Type u_6} [has_add M] [has_add N] :

⇑(add_hom.snd M N) = prod.snd

source

@[protected]

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

M →ₙ* N × P

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

Equations

f.prod g = {to_fun := pi.prod ⇑f ⇑g, map_mul' := _}

source

@[protected]

def add_hom.prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :

add_hom M (N × P)

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

Equations

f.prod g = {to_fun := pi.prod ⇑f ⇑g, map_add' := _}

source

theorem add_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

theorem mul_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

@[simp]

theorem add_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) (x : M) :

⇑(f.prod g) x = (⇑f x, ⇑g x)

source

@[simp]

theorem mul_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) (x : M) :

⇑(f.prod g) x = (⇑f x, ⇑g x)

source

@[simp]

theorem mul_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

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

source

@[simp]

theorem add_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :

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

source

@[simp]

theorem add_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M N) (g : add_hom M P) :

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

source

@[simp]

theorem mul_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N) (g : M →ₙ* P) :

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

source

@[simp]

theorem add_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [has_add P] (f : add_hom M (N × P)) :

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

source

@[simp]

theorem mul_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [has_mul P] (f : M →ₙ* N × P) :

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

source

def add_hom.prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :

add_hom (M × N) (M' × N')

prod.map as an add_monoid_hom

Equations

f.prod_map g = (f.comp (add_hom.fst M N)).prod (g.comp (add_hom.snd M N))

source

def mul_hom.prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

M × N →ₙ* M' × N'

prod.map as a monoid_hom.

Equations

f.prod_map g = (f.comp (mul_hom.fst M N)).prod (g.comp (mul_hom.snd M N))

source

theorem add_hom.prod_map_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :

f.prod_map g = (f.comp (add_hom.fst M N)).prod (g.comp (add_hom.snd M N))

source

theorem mul_hom.prod_map_def {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

f.prod_map g = (f.comp (mul_hom.fst M N)).prod (g.comp (mul_hom.snd M N))

source

@[simp]

theorem add_hom.coe_prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] (f : add_hom M M') (g : add_hom N N') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

@[simp]

theorem mul_hom.coe_prod_map {M : Type u_5} {N : Type u_6} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] (f : M →ₙ* M') (g : N →ₙ* N') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

theorem mul_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [has_mul M] [has_mul N] [has_mul M'] [has_mul N'] [has_mul P] (f : P →ₙ* M) (g : P →ₙ* N) (f' : M →ₙ* M') (g' : N →ₙ* N') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

theorem add_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} {M' : Type u_8} {N' : Type u_9} [has_add M] [has_add N] [has_add M'] [has_add N'] [has_add P] (f : add_hom P M) (g : add_hom P N) (f' : add_hom M M') (g' : add_hom N N') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def mul_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) :

M × N →ₙ* P

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

Equations

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

source

def add_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] (f : add_hom M P) (g : add_hom N P) :

add_hom (M × N) P

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

Equations

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

source

@[simp]

theorem add_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] (f : add_hom M P) (g : add_hom N P) (p : M × N) :

⇑(f.coprod g) p = ⇑f p.fst + ⇑g p.snd

source

@[simp]

theorem mul_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] (f : M →ₙ* P) (g : N →ₙ* P) (p : M × N) :

⇑(f.coprod g) p = ⇑f p.fst * ⇑g p.snd

source

theorem mul_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_mul M] [has_mul N] [comm_semigroup P] {Q : Type u_1} [comm_semigroup Q] (h : P →ₙ* Q) (f : M →ₙ* P) (g : N →ₙ* P) :

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

source

theorem add_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [has_add M] [has_add N] [add_comm_semigroup P] {Q : Type u_1} [add_comm_semigroup Q] (h : add_hom P Q) (f : add_hom M P) (g : add_hom N P) :

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

source

def monoid_hom.fst (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :

M × N →* M

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

Equations

monoid_hom.fst M N = {to_fun := prod.fst N, map_one' := _, map_mul' := _}

source

def add_monoid_hom.fst (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :

M × N →+ M

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

Equations

add_monoid_hom.fst M N = {to_fun := prod.fst N, map_zero' := _, map_add' := _}

source

def monoid_hom.snd (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :

M × N →* N

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

Equations

monoid_hom.snd M N = {to_fun := prod.snd N, map_one' := _, map_mul' := _}

source

def add_monoid_hom.snd (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :

M × N →+ N

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

Equations

add_monoid_hom.snd M N = {to_fun := prod.snd N, map_zero' := _, map_add' := _}

source

def monoid_hom.inl (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :

M →* M × N

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

Equations

monoid_hom.inl M N = {to_fun := λ (x : M), (x, 1), map_one' := _, map_mul' := _}

source

def add_monoid_hom.inl (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :

M →+ M × N

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

Equations

add_monoid_hom.inl M N = {to_fun := λ (x : M), (x, 0), map_zero' := _, map_add' := _}

source

def add_monoid_hom.inr (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] :

N →+ M × N

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

Equations

add_monoid_hom.inr M N = {to_fun := λ (y : N), (0, y), map_zero' := _, map_add' := _}

source

def monoid_hom.inr (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] :

N →* M × N

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

Equations

monoid_hom.inr M N = {to_fun := λ (y : N), (1, y), map_one' := _, map_mul' := _}

source

@[simp]

theorem monoid_hom.coe_fst {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

⇑(monoid_hom.fst M N) = prod.fst

source

@[simp]

theorem add_monoid_hom.coe_fst {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

⇑(add_monoid_hom.fst M N) = prod.fst

source

@[simp]

theorem add_monoid_hom.coe_snd {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

⇑(add_monoid_hom.snd M N) = prod.snd

source

@[simp]

theorem monoid_hom.coe_snd {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

⇑(monoid_hom.snd M N) = prod.snd

source

@[simp]

theorem monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (x : M) :

⇑(monoid_hom.inl M N) x = (x, 1)

source

@[simp]

theorem add_monoid_hom.inl_apply {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (x : M) :

⇑(add_monoid_hom.inl M N) x = (x, 0)

source

@[simp]

theorem monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] (y : N) :

⇑(monoid_hom.inr M N) y = (1, y)

source

@[simp]

theorem add_monoid_hom.inr_apply {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] (y : N) :

⇑(add_monoid_hom.inr M N) y = (0, y)

source

@[simp]

theorem monoid_hom.fst_comp_inl {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

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

source

@[simp]

theorem add_monoid_hom.fst_comp_inl {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

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

source

@[simp]

theorem add_monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

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

source

@[simp]

theorem monoid_hom.snd_comp_inl {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

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

source

@[simp]

theorem add_monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

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

source

@[simp]

theorem monoid_hom.fst_comp_inr {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

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

source

@[simp]

theorem add_monoid_hom.snd_comp_inr {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

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

source

@[simp]

theorem monoid_hom.snd_comp_inr {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

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

source

@[protected]

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

M →+ N × P

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

Equations

f.prod g = {to_fun := pi.prod ⇑f ⇑g, map_zero' := _, map_add' := _}

source

@[protected]

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

M →* N × P

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

Equations

f.prod g = {to_fun := pi.prod ⇑f ⇑g, map_one' := _, map_mul' := _}

source

theorem add_monoid_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

theorem monoid_hom.coe_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :

⇑(f.prod g) = pi.prod ⇑f ⇑g

source

@[simp]

theorem monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) (x : M) :

⇑(f.prod g) x = (⇑f x, ⇑g x)

source

@[simp]

theorem add_monoid_hom.prod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) (x : M) :

⇑(f.prod g) x = (⇑f x, ⇑g x)

source

@[simp]

theorem add_monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :

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

source

@[simp]

theorem monoid_hom.fst_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :

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

source

@[simp]

theorem add_monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N) (g : M →+ P) :

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

source

@[simp]

theorem monoid_hom.snd_comp_prod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N) (g : M →* P) :

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

source

@[simp]

theorem monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [mul_one_class P] (f : M →* N × P) :

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

source

@[simp]

theorem add_monoid_hom.prod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_zero_class P] (f : M →+ N × P) :

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

source

def add_monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :

M × N →+ M' × N'

prod.map as an add_monoid_hom

Equations

f.prod_map g = (f.comp (add_monoid_hom.fst M N)).prod (g.comp (add_monoid_hom.snd M N))

source

def monoid_hom.prod_map {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :

M × N →* M' × N'

prod.map as a monoid_hom.

Equations

f.prod_map g = (f.comp (monoid_hom.fst M N)).prod (g.comp (monoid_hom.snd M N))

source

theorem add_monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :

f.prod_map g = (f.comp (add_monoid_hom.fst M N)).prod (g.comp (add_monoid_hom.snd M N))

source

theorem monoid_hom.prod_map_def {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :

f.prod_map g = (f.comp (monoid_hom.fst M N)).prod (g.comp (monoid_hom.snd M N))

source

@[simp]

theorem monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M →* M') (g : N →* N') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

@[simp]

theorem add_monoid_hom.coe_prod_map {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M →+ M') (g : N →+ N') :

⇑(f.prod_map g) = prod.map ⇑f ⇑g

source

theorem add_monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] [add_zero_class P] (f : P →+ M) (g : P →+ N) (f' : M →+ M') (g' : N →+ N') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

theorem monoid_hom.prod_comp_prod_map {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] [mul_one_class P] (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :

(f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)

source

def monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :

M × N →* P

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

Equations

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

source

def add_monoid_hom.coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :

M × N →+ P

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

Equations

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

source

@[simp]

theorem monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) (p : M × N) :

⇑(f.coprod g) p = ⇑f p.fst * ⇑g p.snd

source

@[simp]

theorem add_monoid_hom.coprod_apply {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) (p : M × N) :

⇑(f.coprod g) p = ⇑f p.fst + ⇑g p.snd

source

@[simp]

theorem add_monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :

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

source

@[simp]

theorem monoid_hom.coprod_comp_inl {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :

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

source

@[simp]

theorem monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M →* P) (g : N →* P) :

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

source

@[simp]

theorem add_monoid_hom.coprod_comp_inr {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M →+ P) (g : N →+ P) :

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

source

@[simp]

theorem monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] (f : M × N →* P) :

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

source

@[simp]

theorem add_monoid_hom.coprod_unique {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] (f : M × N →+ P) :

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

source

@[simp]

theorem add_monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [add_comm_monoid M] [add_comm_monoid N] :

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

source

@[simp]

theorem monoid_hom.coprod_inl_inr {M : Type u_1} {N : Type u_2} [comm_monoid M] [comm_monoid N] :

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

source

theorem add_monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [add_zero_class M] [add_zero_class N] [add_comm_monoid P] {Q : Type u_1} [add_comm_monoid Q] (h : P →+ Q) (f : M →+ P) (g : N →+ P) :

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

source

theorem monoid_hom.comp_coprod {M : Type u_5} {N : Type u_6} {P : Type u_7} [mul_one_class M] [mul_one_class N] [comm_monoid P] {Q : Type u_1} [comm_monoid Q] (h : P →* Q) (f : M →* P) (g : N →* P) :

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

source

def mul_equiv.prod_comm {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

M × N ≃* N × M

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

Equations

mul_equiv.prod_comm = {to_fun := (equiv.prod_comm M N).to_fun, inv_fun := (equiv.prod_comm M N).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.prod_comm {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

M × N ≃+ N × M

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

Equations

add_equiv.prod_comm = {to_fun := (equiv.prod_comm M N).to_fun, inv_fun := (equiv.prod_comm M N).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.coe_prod_comm {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

⇑add_equiv.prod_comm = prod.swap

source

@[simp]

theorem mul_equiv.coe_prod_comm {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

⇑mul_equiv.prod_comm = prod.swap

source

@[simp]

theorem add_equiv.coe_prod_comm_symm {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] :

⇑(add_equiv.prod_comm.symm) = prod.swap

source

@[simp]

theorem mul_equiv.coe_prod_comm_symm {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] :

⇑(mul_equiv.prod_comm.symm) = prod.swap

source

def add_equiv.prod_prod_prod_comm (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] (M' : Type u_8) (N' : Type u_9) [add_zero_class M'] [add_zero_class N'] :

(M × N) × M' × N' ≃+ (M × M') × N × N'

Four-way commutativity of prod. The name matches mul_mul_mul_comm

Equations

add_equiv.prod_prod_prod_comm M N M' N' = {to_fun := λ (mnmn : (M × N) × M' × N'), ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd), inv_fun := λ (mmnn : (M × M') × N × N'), ((mmnn.fst.fst, mmnn.snd.fst), mmnn.fst.snd, mmnn.snd.snd), left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem add_equiv.prod_prod_prod_comm_apply (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] (M' : Type u_8) (N' : Type u_9) [add_zero_class M'] [add_zero_class N'] (mnmn : (M × N) × M' × N') :

⇑(add_equiv.prod_prod_prod_comm M N M' N') mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)

source

@[simp]

theorem mul_equiv.prod_prod_prod_comm_apply (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] (mnmn : (M × N) × M' × N') :

⇑(mul_equiv.prod_prod_prod_comm M N M' N') mnmn = ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd)

source

def mul_equiv.prod_prod_prod_comm (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] :

(M × N) × M' × N' ≃* (M × M') × N × N'

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

Equations

mul_equiv.prod_prod_prod_comm M N M' N' = {to_fun := λ (mnmn : (M × N) × M' × N'), ((mnmn.fst.fst, mnmn.snd.fst), mnmn.fst.snd, mnmn.snd.snd), inv_fun := λ (mmnn : (M × M') × N × N'), ((mmnn.fst.fst, mmnn.snd.fst), mmnn.fst.snd, mmnn.snd.snd), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem mul_equiv.prod_prod_prod_comm_to_equiv (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] :

(mul_equiv.prod_prod_prod_comm M N M' N').to_equiv = equiv.prod_prod_prod_comm M N M' N'

source

@[simp]

theorem add_equiv.sum_sum_sum_comm_to_equiv (M : Type u_5) (N : Type u_6) [add_zero_class M] [add_zero_class N] (M' : Type u_8) (N' : Type u_9) [add_zero_class M'] [add_zero_class N'] :

(add_equiv.prod_prod_prod_comm M N M' N').to_equiv = equiv.prod_prod_prod_comm M N M' N'

source

@[simp]

theorem mul_equiv.prod_prod_prod_comm_symm (M : Type u_5) (N : Type u_6) [mul_one_class M] [mul_one_class N] (M' : Type u_8) (N' : Type u_9) [mul_one_class M'] [mul_one_class N'] :

(mul_equiv.prod_prod_prod_comm M N M' N').symm = mul_equiv.prod_prod_prod_comm M M' N N'

source

def mul_equiv.prod_congr {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] {M' : Type u_8} {N' : Type u_9} [mul_one_class M'] [mul_one_class N'] (f : M ≃* M') (g : N ≃* N') :

M × N ≃* M' × N'

Product of multiplicative isomorphisms; the maps come from equiv.prod_congr.

Equations

f.prod_congr g = {to_fun := (f.to_equiv.prod_congr g.to_equiv).to_fun, inv_fun := (f.to_equiv.prod_congr g.to_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.prod_congr {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] {M' : Type u_8} {N' : Type u_9} [add_zero_class M'] [add_zero_class N'] (f : M ≃+ M') (g : N ≃+ N') :

M × N ≃+ M' × N'

Product of additive isomorphisms; the maps come from equiv.prod_congr.

Equations

f.prod_congr g = {to_fun := (f.to_equiv.prod_congr g.to_equiv).to_fun, inv_fun := (f.to_equiv.prod_congr g.to_equiv).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def add_equiv.unique_prod {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] [unique N] :

N × M ≃+ M

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

Equations

add_equiv.unique_prod = {to_fun := (equiv.unique_prod M N).to_fun, inv_fun := (equiv.unique_prod M N).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.unique_prod {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] [unique N] :

N × M ≃* M

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

Equations

mul_equiv.unique_prod = {to_fun := (equiv.unique_prod M N).to_fun, inv_fun := (equiv.unique_prod M N).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.prod_unique {M : Type u_5} {N : Type u_6} [add_zero_class M] [add_zero_class N] [unique N] :

M × N ≃+ M

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

Equations

add_equiv.prod_unique = {to_fun := (equiv.prod_unique M N).to_fun, inv_fun := (equiv.prod_unique M N).inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

def mul_equiv.prod_unique {M : Type u_5} {N : Type u_6} [mul_one_class M] [mul_one_class N] [unique N] :

M × N ≃* M

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

Equations

mul_equiv.prod_unique = {to_fun := (equiv.prod_unique M N).to_fun, inv_fun := (equiv.prod_unique M N).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def add_equiv.prod_add_units {M : Type u_5} {N : Type u_6} [add_monoid M] [add_monoid N] :

add_units (M × N) ≃+ add_units M × add_units 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