# Coproduct (free product) of two monoids or groups #

In this file we define Monoid.Coprod M N (notation: M ∗ N) to be the coproduct (a.k.a. free product) of two monoids. The same type is used for the coproduct of two monoids and for the coproduct of two groups.

The coproduct M ∗ N has the following universal property: for any monoid P and homomorphisms f : M →* P, g : N →* P, there exists a unique homomorphism fg : M ∗ N →* P such that fg ∘ Monoid.Coprod.inl = f and fg ∘ Monoid.Coprod.inr = g, where Monoid.Coprod.inl : M →* M ∗ N and Monoid.Coprod.inr : N →* M ∗ N are canonical embeddings. This homomorphism fg is given by Monoid.Coprod.lift f g.

We also define some homomorphisms and isomorphisms about M ∗ N, and provide additive versions of all definitions and theorems.

## Main definitions #

### Types #

• Monoid.Coprod M N (a.k.a. M ∗ N): the free product (a.k.a. coproduct) of two monoids M and N.
• AddMonoid.Coprod M N (no notation): the additive version of Monoid.Coprod.

In other sections, we only list multiplicative definitions.

### Instances #

• MulOneClass, Monoid, and Group structures on the coproduct M ∗ N.

### Monoid homomorphisms #

• Monoid.Coprod.mk: the projection FreeMonoid (M ⊕ N) →* M ∗ N.

• Monoid.Coprod.inl, Monoid.Coprod.inr: canonical embeddings M →* M ∗ N and N →* M ∗ N.

• Monoid.Coprod.lift: construct a monoid homomorphism M ∗ N →* P from homomorphisms M →* P and N →* P; see also Monoid.Coprod.liftEquiv.

• Monoid.Coprod.clift: a constructor for homomorphisms M ∗ N →* P that allows the user to control the computational behavior.

• Monoid.Coprod.map: combine two homomorphisms f : M →* N and g : M' →* N' into M ∗ M' →* N ∗ N'.

• Monoid.Coprod.swap: the natural homomorphism M ∗ N →* N ∗ M.

• Monoid.Coprod.fst, Monoid.Coprod.snd, and Monoid.Coprod.toProd: natural projections M ∗ N →* M, M ∗ N →* N, and M ∗ N →* M × N.

### Monoid isomorphisms #

• MulEquiv.coprodCongr: a MulEquiv version of Monoid.Coprod.map.
• MulEquiv.coprodComm: a MulEquiv version of Monoid.Coprod.swap.
• MulEquiv.coprodAssoc: associativity of the coproduct.
• MulEquiv.coprodPUnit, MulEquiv.punitCoprod: free product by PUnit on the left or on the right is isomorphic to the original monoid.

## Main results #

The universal property of the coproduct is given by the definition Monoid.Coprod.lift and the lemma Monoid.Coprod.lift_unique.

We also prove a slightly more general extensionality lemma Monoid.Coprod.hom_ext for homomorphisms M ∗ N →* P and prove lots of basic lemmas like Monoid.Coprod.fst_comp_inl.

## Implementation details #

The definition of the coproduct of an indexed family of monoids is formalized in Monoid.CoprodI. While mathematically M ∗ N is a particular case of the coproduct of an indexed family of monoids, it is easier to build API from scratch instead of using something like

def Monoid.Coprod M N := Monoid.CoprodI ![M, N]


or

def Monoid.Coprod M N := Monoid.CoprodI (fun b : Bool => cond b M N)


There are several reasons to build an API from scratch.

• API about Con makes it easy to define the required type and prove the universal property, so there is little overhead compared to transferring API from Monoid.CoprodI.
• If M and N live in different universes, then the definition has to add ULifts; this makes it harder to transfer API and definitions.
• As of now, we have no way to automatically build an instance of (k : Fin 2) → Monoid (![M, N] k) from [Monoid M] and [Monoid N], not even speaking about more advanced typeclass assumptions that involve both M and N.
• Using a list of M ⊕ N instead of, e.g., a list of Σ k : Fin 2, ![M, N] k as the underlying type makes it possible to write computationally effective code (though this point is not tested yet).

## TODO #

• Prove Monoid.CoprodI (f : Fin 2 → Type*) ≃* f 0 ∗ f 1 and Monoid.CoprodI (f : Bool → Type*) ≃* f false ∗ f true.

## Tags #

group, monoid, coproduct, free product

def AddMonoid.coprodCon (M : Type u_1) (N : Type u_2) [] [] :

The minimal additive congruence relation c on FreeAddMonoid (M ⊕ N) such that FreeAddMonoid.of ∘ Sum.inl and FreeAddMonoid.of ∘ Sum.inr are additive monoid homomorphisms to the quotient by c.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Monoid.coprodCon (M : Type u_1) (N : Type u_2) [] [] :

The minimal congruence relation c on FreeMonoid (M ⊕ N) such that FreeMonoid.of ∘ Sum.inl and FreeMonoid.of ∘ Sum.inr are monoid homomorphisms to the quotient by c.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def AddMonoid.Coprod (M : Type u_1) (N : Type u_2) [] [] :
Type (max u_1 u_2)

Coproduct of two additive monoids or groups.

Equations
• = ().Quotient
Instances For
def Monoid.Coprod (M : Type u_1) (N : Type u_2) [] [] :
Type (max u_1 u_2)

Coproduct of two monoids or groups.

Equations
• = ().Quotient
Instances For

Coproduct of two monoids or groups.

Equations
Instances For
instance AddMonoid.Coprod.instAddZeroClass {M : Type u_1} {N : Type u_2} [] [] :
Equations
instance Monoid.Coprod.instMulOneClass {M : Type u_1} {N : Type u_2} [] [] :
Equations
• Monoid.Coprod.instMulOneClass = ().mulOneClass
def AddMonoid.Coprod.mk {M : Type u_1} {N : Type u_2} [] [] :

The natural projection FreeAddMonoid (M ⊕ N) →+ AddMonoid.Coprod M N.

Equations
Instances For
def Monoid.Coprod.mk {M : Type u_1} {N : Type u_2} [] [] :

The natural projection FreeMonoid (M ⊕ N) →* M ∗ N.

Equations
• Monoid.Coprod.mk = ().mk'
Instances For
@[simp]
theorem AddMonoid.Coprod.con_ker_mk {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.con_ker_mk {M : Type u_1} {N : Type u_2} [] [] :
Con.ker Monoid.Coprod.mk =
theorem AddMonoid.Coprod.mk_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.mk_surjective {M : Type u_1} {N : Type u_2} [] [] :
Function.Surjective Monoid.Coprod.mk
@[simp]
theorem AddMonoid.Coprod.mrange_mk {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.mrange_mk {M : Type u_1} {N : Type u_2} [] [] :
MonoidHom.mrange Monoid.Coprod.mk =
theorem AddMonoid.Coprod.mk_eq_mk {M : Type u_1} {N : Type u_2} [] [] {w₁ : FreeAddMonoid (M N)} {w₂ : FreeAddMonoid (M N)} :
theorem Monoid.Coprod.mk_eq_mk {M : Type u_1} {N : Type u_2} [] [] {w₁ : FreeMonoid (M N)} {w₂ : FreeMonoid (M N)} :
Monoid.Coprod.mk w₁ = Monoid.Coprod.mk w₂ () w₁ w₂
def AddMonoid.Coprod.inl {M : Type u_1} {N : Type u_2} [] [] :
M →+

The natural embedding M →+ AddMonoid.Coprod M N.

Equations
• AddMonoid.Coprod.inl = { toFun := fun (x : M) => AddMonoid.Coprod.mk (), map_zero' := , map_add' := }
Instances For
theorem AddMonoid.Coprod.inl.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoid.Coprod.inl.proof_2 {M : Type u_1} {N : Type u_2} [] [] (x : M) (y : M) :
def Monoid.Coprod.inl {M : Type u_1} {N : Type u_2} [] [] :
M →*

The natural embedding M →* M ∗ N.

Equations
• Monoid.Coprod.inl = { toFun := fun (x : M) => Monoid.Coprod.mk (), map_one' := , map_mul' := }
Instances For
theorem AddMonoid.Coprod.inr.proof_2 {M : Type u_1} {N : Type u_2} [] [] (x : N) (y : N) :
def AddMonoid.Coprod.inr {M : Type u_1} {N : Type u_2} [] [] :
N →+

The natural embedding N →+ AddMonoid.Coprod M N.

Equations
• AddMonoid.Coprod.inr = { toFun := fun (x : N) => AddMonoid.Coprod.mk (), map_zero' := , map_add' := }
Instances For
theorem AddMonoid.Coprod.inr.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
def Monoid.Coprod.inr {M : Type u_1} {N : Type u_2} [] [] :
N →*

The natural embedding N →* M ∗ N.

Equations
• Monoid.Coprod.inr = { toFun := fun (x : N) => Monoid.Coprod.mk (), map_one' := , map_mul' := }
Instances For
@[simp]
theorem AddMonoid.Coprod.mk_of_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
@[simp]
theorem Monoid.Coprod.mk_of_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
Monoid.Coprod.mk () = Monoid.Coprod.inl x
@[simp]
theorem AddMonoid.Coprod.mk_of_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
@[simp]
theorem Monoid.Coprod.mk_of_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
Monoid.Coprod.mk () = Monoid.Coprod.inr x
theorem AddMonoid.Coprod.induction_on' {M : Type u_1} {N : Type u_2} [] [] {C : Prop} (m : ) (one : C 0) (inl_mul : ∀ (m : M) (x : ), C xC (AddMonoid.Coprod.inl m + x)) (inr_mul : ∀ (n : N) (x : ), C xC (AddMonoid.Coprod.inr n + x)) :
C m
theorem Monoid.Coprod.induction_on' {M : Type u_1} {N : Type u_2} [] [] {C : Prop} (m : ) (one : C 1) (inl_mul : ∀ (m : M) (x : ), C xC (Monoid.Coprod.inl m * x)) (inr_mul : ∀ (n : N) (x : ), C xC (Monoid.Coprod.inr n * x)) :
C m
theorem AddMonoid.Coprod.induction_on {M : Type u_1} {N : Type u_2} [] [] {C : Prop} (m : ) (inl : ∀ (m : M), C (AddMonoid.Coprod.inl m)) (inr : ∀ (n : N), C (AddMonoid.Coprod.inr n)) (mul : ∀ (x y : ), C xC yC (x + y)) :
C m
theorem Monoid.Coprod.induction_on {M : Type u_1} {N : Type u_2} [] [] {C : Prop} (m : ) (inl : ∀ (m : M), C (Monoid.Coprod.inl m)) (inr : ∀ (n : N), C (Monoid.Coprod.inr n)) (mul : ∀ (x y : ), C xC yC (x * y)) :
C m
theorem AddMonoid.Coprod.clift.proof_1 {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) :
sInf {c : AddCon (FreeAddMonoid (M N)) | (∀ (x y : M), c (FreeAddMonoid.of (Sum.inl (x + y))) ()) (∀ (x y : N), c (FreeAddMonoid.of (Sum.inr (x + y))) ()) c () 0 c () 0}
def AddMonoid.Coprod.clift {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) :
→+ P

Lift an additive monoid homomorphism FreeAddMonoid (M ⊕ N) →+ P satisfying additional properties to AddMonoid.Coprod M N →+ P.

Compared to AddMonoid.Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs AddZeroclass assumptions while AddMonoid.Coprod.lift needs an AddMonoid structure.

Equations
Instances For
def Monoid.Coprod.clift {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeMonoid (M N) →* P) (hM₁ : f () = 1) (hN₁ : f () = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f ()) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f ()) :
→* P

Lift a monoid homomorphism FreeMonoid (M ⊕ N) →* P satisfying additional properties to M ∗ N →* P. In many cases, Coprod.lift is more convenient.

Compared to Coprod.lift, this definition allows a user to provide a custom computational behavior. Also, it only needs MulOneclass assumptions while Coprod.lift needs a Monoid structure.

Equations
Instances For
@[simp]
theorem AddMonoid.Coprod.clift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) (x : M) :
@[simp]
theorem Monoid.Coprod.clift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeMonoid (M N) →* P) (hM₁ : f () = 1) (hN₁ : f () = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f ()) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f ()) (x : M) :
(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inl x) = f ()
@[simp]
theorem AddMonoid.Coprod.clift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) (x : N) :
@[simp]
theorem Monoid.Coprod.clift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeMonoid (M N) →* P) (hM₁ : f () = 1) (hN₁ : f () = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f ()) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f ()) (x : N) :
(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.inr x) = f ()
@[simp]
theorem AddMonoid.Coprod.clift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) (w : FreeAddMonoid (M N)) :
@[simp]
theorem Monoid.Coprod.clift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeMonoid (M N) →* P) (hM₁ : f () = 1) (hN₁ : f () = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f ()) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f ()) (w : FreeMonoid (M N)) :
(Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.mk w) = f w
@[simp]
theorem AddMonoid.Coprod.clift_comp_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeAddMonoid (M N) →+ P) (hM₁ : f () = 0) (hN₁ : f () = 0) (hM : ∀ (x y : M), f (FreeAddMonoid.of (Sum.inl (x + y))) = f ()) (hN : ∀ (x y : N), f (FreeAddMonoid.of (Sum.inr (x + y))) = f ()) :
@[simp]
theorem Monoid.Coprod.clift_comp_mk {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : FreeMonoid (M N) →* P) (hM₁ : f () = 1) (hN₁ : f () = 1) (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f ()) (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f ()) :
(Monoid.Coprod.clift f hM₁ hN₁ hM hN).comp Monoid.Coprod.mk = f
@[simp]
theorem AddMonoid.Coprod.mclosure_range_inl_union_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.mclosure_range_inl_union_inr {M : Type u_1} {N : Type u_2} [] [] :
Submonoid.closure (Set.range Monoid.Coprod.inl Set.range Monoid.Coprod.inr) =
@[simp]
theorem AddMonoid.Coprod.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.mrange_inl_sup_mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
MonoidHom.mrange Monoid.Coprod.inl MonoidHom.mrange Monoid.Coprod.inr =
theorem AddMonoid.Coprod.codisjoint_mrange_inl_mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.codisjoint_mrange_inl_mrange_inr {M : Type u_1} {N : Type u_2} [] [] :
Codisjoint (MonoidHom.mrange Monoid.Coprod.inl) (MonoidHom.mrange Monoid.Coprod.inr)
theorem AddMonoid.Coprod.mrange_eq {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : →+ P) :
theorem Monoid.Coprod.mrange_eq {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] (f : →* P) :
= MonoidHom.mrange (f.comp Monoid.Coprod.inl) MonoidHom.mrange (f.comp Monoid.Coprod.inr)
theorem AddMonoid.Coprod.hom_ext {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] {f : →+ P} {g : →+ P} (h₁ : f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl) (h₂ : f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr) :
f = g

Extensionality lemma for additive monoid homomorphisms AddMonoid.Coprod M N →+ P. If two homomorphisms agree on the ranges of AddMonoid.Coprod.inl and AddMonoid.Coprod.inr, then they are equal.

theorem Monoid.Coprod.hom_ext {M : Type u_1} {N : Type u_2} {P : Type u_5} [] [] [] {f : →* P} {g : →* P} (h₁ : f.comp Monoid.Coprod.inl = g.comp Monoid.Coprod.inl) (h₂ : f.comp Monoid.Coprod.inr = g.comp Monoid.Coprod.inr) :
f = g

Extensionality lemma for monoid homomorphisms M ∗ N →* P. If two homomorphisms agree on the ranges of Monoid.Coprod.inl and Monoid.Coprod.inr, then they are equal.

@[simp]
theorem AddMonoid.Coprod.clift_mk {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.clift_mk {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.clift Monoid.Coprod.mk =
theorem AddMonoid.Coprod.map.proof_4 {M : Type u_4} {N : Type u_3} {M' : Type u_1} {N' : Type u_2} [] [] [] [] (f : M →+ M') (g : N →+ N') (x : N) (y : N) :
def AddMonoid.Coprod.map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') :

Map AddMonoid.Coprod M N to AddMonoid.Coprod M' N' by applying Sum.map f g to each element of the underlying list.

Equations
Instances For
theorem AddMonoid.Coprod.map.proof_2 {N : Type u_3} {M' : Type u_1} {N' : Type u_2} [] [] [] (g : N →+ N') :
theorem AddMonoid.Coprod.map.proof_1 {M : Type u_3} {M' : Type u_1} {N' : Type u_2} [] [] [] (f : M →+ M') :
theorem AddMonoid.Coprod.map.proof_3 {M : Type u_3} {N : Type u_4} {M' : Type u_1} {N' : Type u_2} [] [] [] [] (f : M →+ M') (g : N →+ N') (x : M) (y : M) :
def Monoid.Coprod.map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') :

Map M ∗ N to M' ∗ N' by applying Sum.map f g to each element of the underlying list.

Equations
Instances For
@[simp]
theorem AddMonoid.Coprod.map_mk_ofList {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') (l : List (M N)) :
@[simp]
theorem Monoid.Coprod.map_mk_ofList {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') (l : List (M N)) :
() (Monoid.Coprod.mk (FreeMonoid.ofList l)) = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map f g) l))
@[simp]
theorem AddMonoid.Coprod.map_apply_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') (x : M) :
@[simp]
theorem Monoid.Coprod.map_apply_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') (x : M) :
() (Monoid.Coprod.inl x) = Monoid.Coprod.inl (f x)
@[simp]
theorem AddMonoid.Coprod.map_apply_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') (x : N) :
@[simp]
theorem Monoid.Coprod.map_apply_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') (x : N) :
() (Monoid.Coprod.inr x) = Monoid.Coprod.inr (g x)
@[simp]
theorem AddMonoid.Coprod.map_comp_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') :
@[simp]
theorem Monoid.Coprod.map_comp_inl {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') :
().comp Monoid.Coprod.inl = Monoid.Coprod.inl.comp f
@[simp]
theorem AddMonoid.Coprod.map_comp_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') :
@[simp]
theorem Monoid.Coprod.map_comp_inr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') :
().comp Monoid.Coprod.inr = Monoid.Coprod.inr.comp g
@[simp]
theorem AddMonoid.Coprod.map_id_id {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.map_id_id {M : Type u_1} {N : Type u_2} [] [] :
=
theorem AddMonoid.Coprod.map_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] {M'' : Type u_6} {N'' : Type u_7} [AddZeroClass M''] [AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N') :
().comp () = AddMonoid.Coprod.map (f'.comp f) (g'.comp g)
theorem Monoid.Coprod.map_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] {M'' : Type u_6} {N'' : Type u_7} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N') :
().comp () = Monoid.Coprod.map (f'.comp f) (g'.comp g)
theorem AddMonoid.Coprod.map_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] {M'' : Type u_6} {N'' : Type u_7} [AddZeroClass M''] [AddZeroClass N''] (f' : M' →+ M'') (g' : N' →+ N'') (f : M →+ M') (g : N →+ N') (x : ) :
() (() x) = (AddMonoid.Coprod.map (f'.comp f) (g'.comp g)) x
theorem Monoid.Coprod.map_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] {M'' : Type u_6} {N'' : Type u_7} [MulOneClass M''] [MulOneClass N''] (f' : M' →* M'') (g' : N' →* N'') (f : M →* M') (g : N →* N') (x : ) :
() (() x) = (Monoid.Coprod.map (f'.comp f) (g'.comp g)) x
def AddMonoid.Coprod.swap (M : Type u_1) (N : Type u_2) [] [] :

Map AddMonoid.Coprod M N to AddMonoid.Coprod N M by applying Sum.swap to each element of the underlying list.

See also AddEquiv.coprodComm for an AddEquiv version.

Equations
Instances For
theorem AddMonoid.Coprod.swap.proof_4 (M : Type u_1) (N : Type u_2) [] [] (x : N) (y : N) :
theorem AddMonoid.Coprod.swap.proof_3 (M : Type u_1) (N : Type u_2) [] [] (x : M) (y : M) :
theorem AddMonoid.Coprod.swap.proof_2 (M : Type u_1) (N : Type u_2) [] [] :
theorem AddMonoid.Coprod.swap.proof_1 (M : Type u_1) (N : Type u_2) [] [] :
def Monoid.Coprod.swap (M : Type u_1) (N : Type u_2) [] [] :

Map M ∗ N to N ∗ M by applying Sum.swap to each element of the underlying list.

See also MulEquiv.coprodComm for a MulEquiv version.

Equations
Instances For
@[simp]
theorem AddMonoid.Coprod.swap_comp_swap (M : Type u_1) (N : Type u_2) [] [] :
().comp () =
@[simp]
theorem Monoid.Coprod.swap_comp_swap (M : Type u_1) (N : Type u_2) [] [] :
().comp () =
@[simp]
theorem AddMonoid.Coprod.swap_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
() (() x) = x
@[simp]
theorem Monoid.Coprod.swap_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
() (() x) = x
theorem AddMonoid.Coprod.swap_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') :
().comp () = ().comp ()
theorem Monoid.Coprod.swap_comp_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') :
().comp () = ().comp ()
theorem AddMonoid.Coprod.swap_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →+ M') (g : N →+ N') (x : ) :
() (() x) = () (() x)
theorem Monoid.Coprod.swap_map {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (f : M →* M') (g : N →* N') (x : ) :
() (() x) = () (() x)
@[simp]
theorem AddMonoid.Coprod.swap_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.swap_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
().comp Monoid.Coprod.inl = Monoid.Coprod.inr
@[simp]
theorem AddMonoid.Coprod.swap_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
@[simp]
theorem Monoid.Coprod.swap_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
() (Monoid.Coprod.inl x) = Monoid.Coprod.inr x
@[simp]
theorem AddMonoid.Coprod.swap_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.swap_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
().comp Monoid.Coprod.inr = Monoid.Coprod.inl
@[simp]
theorem AddMonoid.Coprod.swap_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
@[simp]
theorem Monoid.Coprod.swap_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
() (Monoid.Coprod.inr x) = Monoid.Coprod.inl x
theorem AddMonoid.Coprod.swap_injective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.swap_injective {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoid.Coprod.swap_inj {M : Type u_1} {N : Type u_2} [] [] {x : } {y : } :
() x = () y x = y
@[simp]
theorem Monoid.Coprod.swap_inj {M : Type u_1} {N : Type u_2} [] [] {x : } {y : } :
() x = () y x = y
@[simp]
theorem AddMonoid.Coprod.swap_eq_zero {M : Type u_1} {N : Type u_2} [] [] {x : } :
() x = 0 x = 0
@[simp]
theorem Monoid.Coprod.swap_eq_one {M : Type u_1} {N : Type u_2} [] [] {x : } :
() x = 1 x = 1
theorem AddMonoid.Coprod.swap_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.swap_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoid.Coprod.swap_bijective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.swap_bijective {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoid.Coprod.mker_swap {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.mker_swap {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem AddMonoid.Coprod.mrange_swap {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.mrange_swap {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoid.Coprod.lift.proof_3 {M : Type u_2} {P : Type u_1} [] [] (f : M →+ P) (x : M) (y : M) :
f (x + y) = f x + f y
theorem AddMonoid.Coprod.lift.proof_2 {N : Type u_2} {P : Type u_1} [] [] (g : N →+ P) :
g 0 = 0
def AddMonoid.Coprod.lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) :
→+ P

Lift a pair of additive monoid homomorphisms f : M →+ P, g : N →+ P to an additive monoid homomorphism AddMonoid.Coprod M N →+ P.

See also AddMonoid.Coprod.clift for a version that allows custom computational behavior and works for an AddZeroClass codomain.

Equations
Instances For
theorem AddMonoid.Coprod.lift.proof_4 {N : Type u_2} {P : Type u_1} [] [] (g : N →+ P) (x : N) (y : N) :
g (x + y) = g x + g y
theorem AddMonoid.Coprod.lift.proof_1 {M : Type u_2} {P : Type u_1} [] [] (f : M →+ P) :
f 0 = 0
def Monoid.Coprod.lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) :
→* P

Lift a pair of monoid homomorphisms f : M →* P, g : N →* P to a monoid homomorphism M ∗ N →* P.

See also Coprod.clift for a version that allows custom computational behavior and works for a MulOneClass codomain.

Equations
Instances For
@[simp]
theorem AddMonoid.Coprod.lift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) (x : FreeAddMonoid (M N)) :
@[simp]
theorem Monoid.Coprod.lift_apply_mk {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) (x : FreeMonoid (M N)) :
() (Monoid.Coprod.mk x) = (FreeMonoid.lift (Sum.elim f g)) x
@[simp]
theorem AddMonoid.Coprod.lift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) (x : M) :
() (AddMonoid.Coprod.inl x) = f x
@[simp]
theorem Monoid.Coprod.lift_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) (x : M) :
() (Monoid.Coprod.inl x) = f x
theorem AddMonoid.Coprod.lift_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] {f : M →+ P} {g : N →+ P} {fg : →+ P} (h₁ : fg.comp AddMonoid.Coprod.inl = f) (h₂ : fg.comp AddMonoid.Coprod.inr = g) :
fg =
theorem Monoid.Coprod.lift_unique {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] {f : M →* P} {g : N →* P} {fg : →* P} (h₁ : fg.comp Monoid.Coprod.inl = f) (h₂ : fg.comp Monoid.Coprod.inr = g) :
fg =
@[simp]
theorem AddMonoid.Coprod.lift_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) :
@[simp]
theorem Monoid.Coprod.lift_comp_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) :
().comp Monoid.Coprod.inl = f
@[simp]
theorem AddMonoid.Coprod.lift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) (x : N) :
() (AddMonoid.Coprod.inr x) = g x
@[simp]
theorem Monoid.Coprod.lift_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) (x : N) :
() (Monoid.Coprod.inr x) = g x
@[simp]
theorem AddMonoid.Coprod.lift_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) :
@[simp]
theorem Monoid.Coprod.lift_comp_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) :
().comp Monoid.Coprod.inr = g
@[simp]
theorem AddMonoid.Coprod.lift_comp_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) :
().comp () =
@[simp]
theorem Monoid.Coprod.lift_comp_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) :
().comp () =
@[simp]
theorem AddMonoid.Coprod.lift_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) (x : ) :
() (() x) = () x
@[simp]
theorem Monoid.Coprod.lift_swap {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) (x : ) :
() (() x) = () x
theorem AddMonoid.Coprod.comp_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] {P' : Type u_4} [] (f : P →+ P') (g₁ : M →+ P) (g₂ : N →+ P) :
f.comp () = AddMonoid.Coprod.lift (f.comp g₁) (f.comp g₂)
theorem Monoid.Coprod.comp_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] {P' : Type u_4} [Monoid P'] (f : P →* P') (g₁ : M →* P) (g₂ : N →* P) :
f.comp () = Monoid.Coprod.lift (f.comp g₁) (f.comp g₂)
def AddMonoid.Coprod.liftEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] :
(M →+ P) × (N →+ P) ( →+ P)

AddMonoid.Coprod.lift as an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoid.Coprod.liftEquiv.proof_1 {M : Type u_2} {N : Type u_3} {P : Type u_1} [] [] [] :
∀ (x : (M →+ P) × (N →+ P)), (fun (f : →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) ((fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) x) = (fun (f : →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) ((fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) x)
theorem AddMonoid.Coprod.liftEquiv.proof_2 {M : Type u_2} {N : Type u_1} {P : Type u_3} [] [] [] :
∀ (x : →+ P), (fun (fg : (M →+ P) × (N →+ P)) => AddMonoid.Coprod.lift fg.1 fg.2) ((fun (f : →+ P) => (f.comp AddMonoid.Coprod.inl, f.comp AddMonoid.Coprod.inr)) x) = x
def Monoid.Coprod.liftEquiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] :
(M →* P) × (N →* P) ( →* P)

Coprod.lift as an equivalence.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddMonoid.Coprod.mrange_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →+ P) (g : N →+ P) :
@[simp]
theorem Monoid.Coprod.mrange_lift {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (f : M →* P) (g : N →* P) :
theorem AddMonoid.Coprod.inst.proof_1 {M : Type u_1} {N : Type u_2} [] [] (a : ().Quotient) (b : ().Quotient) (c : ().Quotient) :
a + b + c = a + (b + c)
theorem AddMonoid.Coprod.inst.proof_3 {M : Type u_1} {N : Type u_2} [] [] (a : ().Quotient) :
a + 0 = a
instance AddMonoid.Coprod.inst {M : Type u_1} {N : Type u_2} [] [] :
Equations
theorem AddMonoid.Coprod.inst.proof_5 {M : Type u_1} {N : Type u_2} [] [] :
∀ (n : ) (x : ), nsmulRec (n + 1) x = nsmulRec (n + 1) x
theorem AddMonoid.Coprod.inst.proof_2 {M : Type u_1} {N : Type u_2} [] [] (a : ().Quotient) :
0 + a = a
theorem AddMonoid.Coprod.inst.proof_4 {M : Type u_1} {N : Type u_2} [] [] :
∀ (x : ), nsmulRec 0 x = nsmulRec 0 x
instance Monoid.Coprod.inst {M : Type u_1} {N : Type u_2} [] [] :
Equations
• Monoid.Coprod.inst = Monoid.mk npowRec
def AddMonoid.Coprod.fst {M : Type u_1} {N : Type u_2} [] [] :
→+ M

The natural projection AddMonoid.Coprod M N →+ M.

Equations
Instances For
def Monoid.Coprod.fst {M : Type u_1} {N : Type u_2} [] [] :
→* M

The natural projection M ∗ N →* M.

Equations
• Monoid.Coprod.fst =
Instances For
def AddMonoid.Coprod.snd {M : Type u_1} {N : Type u_2} [] [] :
→+ N

The natural projection AddMonoid.Coprod M N →+ N.

Equations
Instances For
def Monoid.Coprod.snd {M : Type u_1} {N : Type u_2} [] [] :
→* N

The natural projection M ∗ N →* N.

Equations
• Monoid.Coprod.snd =
Instances For
def AddMonoid.Coprod.toSum {M : Type u_1} {N : Type u_2} [] [] :
→+ M × N

The natural projection AddMonoid.Coprod M N →+ M × N.

Equations
Instances For
def Monoid.Coprod.toProd {M : Type u_1} {N : Type u_2} [] [] :
→* M × N

The natural projection M ∗ N →* M × N.

Equations
Instances For
@[simp]
theorem AddMonoid.Coprod.fst_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.fst_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.fst.comp Monoid.Coprod.inl =
@[simp]
theorem AddMonoid.Coprod.fst_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
@[simp]
theorem Monoid.Coprod.fst_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
Monoid.Coprod.fst (Monoid.Coprod.inl x) = x
@[simp]
theorem AddMonoid.Coprod.fst_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.fst_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.fst.comp Monoid.Coprod.inr = 1
@[simp]
theorem AddMonoid.Coprod.fst_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
@[simp]
theorem Monoid.Coprod.fst_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
Monoid.Coprod.fst (Monoid.Coprod.inr x) = 1
@[simp]
theorem AddMonoid.Coprod.snd_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.snd_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.snd.comp Monoid.Coprod.inl = 1
@[simp]
theorem AddMonoid.Coprod.snd_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
@[simp]
theorem Monoid.Coprod.snd_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
Monoid.Coprod.snd (Monoid.Coprod.inl x) = 1
@[simp]
theorem AddMonoid.Coprod.snd_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.snd_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.snd.comp Monoid.Coprod.inr =
@[simp]
theorem AddMonoid.Coprod.snd_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
@[simp]
theorem Monoid.Coprod.snd_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
Monoid.Coprod.snd (Monoid.Coprod.inr x) = x
@[simp]
theorem AddMonoid.Coprod.toSum_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.toProd_comp_inl {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.toProd.comp Monoid.Coprod.inl =
@[simp]
theorem AddMonoid.Coprod.toSum_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.toProd_comp_inr {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.toProd.comp Monoid.Coprod.inr =
@[simp]
theorem AddMonoid.Coprod.toSum_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
@[simp]
theorem Monoid.Coprod.toProd_apply_inl {M : Type u_1} {N : Type u_2} [] [] (x : M) :
Monoid.Coprod.toProd (Monoid.Coprod.inl x) = (x, 1)
@[simp]
theorem AddMonoid.Coprod.toSum_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
@[simp]
theorem Monoid.Coprod.toProd_apply_inr {M : Type u_1} {N : Type u_2} [] [] (x : N) :
Monoid.Coprod.toProd (Monoid.Coprod.inr x) = (1, x)
@[simp]
theorem AddMonoid.Coprod.fst_sum_snd {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.fst_prod_snd {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.fst.prod Monoid.Coprod.snd = Monoid.Coprod.toProd
@[simp]
theorem AddMonoid.Coprod.sum_mk_fst_snd {M : Type u_1} {N : Type u_2} [] [] (x : ) :
@[simp]
theorem Monoid.Coprod.prod_mk_fst_snd {M : Type u_1} {N : Type u_2} [] [] (x : ) :
(Monoid.Coprod.fst x, Monoid.Coprod.snd x) = Monoid.Coprod.toProd x
@[simp]
theorem AddMonoid.Coprod.fst_comp_toSum {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.fst_comp_toProd {M : Type u_1} {N : Type u_2} [] [] :
().comp Monoid.Coprod.toProd = Monoid.Coprod.fst
@[simp]
theorem AddMonoid.Coprod.fst_toSum {M : Type u_1} {N : Type u_2} [] [] (x : ) :
@[simp]
theorem Monoid.Coprod.fst_toProd {M : Type u_1} {N : Type u_2} [] [] (x : ) :
(Monoid.Coprod.toProd x).1 = Monoid.Coprod.fst x
@[simp]
theorem AddMonoid.Coprod.snd_comp_toSum {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.snd_comp_toProd {M : Type u_1} {N : Type u_2} [] [] :
().comp Monoid.Coprod.toProd = Monoid.Coprod.snd
@[simp]
theorem AddMonoid.Coprod.snd_toSum {M : Type u_1} {N : Type u_2} [] [] (x : ) :
@[simp]
theorem Monoid.Coprod.snd_toProd {M : Type u_1} {N : Type u_2} [] [] (x : ) :
(Monoid.Coprod.toProd x).2 = Monoid.Coprod.snd x
@[simp]
theorem AddMonoid.Coprod.fst_comp_swap {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.fst_comp_swap {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.fst.comp () = Monoid.Coprod.snd
@[simp]
theorem AddMonoid.Coprod.fst_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
@[simp]
theorem Monoid.Coprod.fst_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
Monoid.Coprod.fst (() x) = Monoid.Coprod.snd x
@[simp]
theorem AddMonoid.Coprod.snd_comp_swap {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.snd_comp_swap {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.snd.comp () = Monoid.Coprod.fst
@[simp]
theorem AddMonoid.Coprod.snd_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
@[simp]
theorem Monoid.Coprod.snd_swap {M : Type u_1} {N : Type u_2} [] [] (x : ) :
Monoid.Coprod.snd (() x) = Monoid.Coprod.fst x
@[simp]
theorem AddMonoid.Coprod.lift_inr_inl {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.lift_inr_inl {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.lift Monoid.Coprod.inr Monoid.Coprod.inl =
@[simp]
theorem AddMonoid.Coprod.lift_inl_inr {M : Type u_1} {N : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.lift_inl_inr {M : Type u_1} {N : Type u_2} [] [] :
Monoid.Coprod.lift Monoid.Coprod.inl Monoid.Coprod.inr =
theorem AddMonoid.Coprod.inl_injective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.inl_injective {M : Type u_1} {N : Type u_2} [] [] :
Function.Injective Monoid.Coprod.inl
theorem AddMonoid.Coprod.inr_injective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.inr_injective {M : Type u_1} {N : Type u_2} [] [] :
Function.Injective Monoid.Coprod.inr
theorem AddMonoid.Coprod.fst_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.fst_surjective {M : Type u_1} {N : Type u_2} [] [] :
Function.Surjective Monoid.Coprod.fst
theorem AddMonoid.Coprod.snd_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.snd_surjective {M : Type u_1} {N : Type u_2} [] [] :
Function.Surjective Monoid.Coprod.snd
theorem AddMonoid.Coprod.toSum_surjective {M : Type u_1} {N : Type u_2} [] [] :
theorem Monoid.Coprod.toProd_surjective {M : Type u_1} {N : Type u_2} [] [] :
Function.Surjective Monoid.Coprod.toProd
theorem AddMonoid.Coprod.mk_of_neg_add {G : Type u_1} {H : Type u_2} [] [] (x : G H) :
abbrev AddMonoid.Coprod.mk_of_neg_add.match_1 {G : Type u_1} {H : Type u_2} (motive : G HProp) :
∀ (x : G H), (∀ (val : G), motive (Sum.inl val))(∀ (val : H), motive (Sum.inr val))motive x
Equations
• =
Instances For
theorem Monoid.Coprod.mk_of_inv_mul {G : Type u_1} {H : Type u_2} [] [] (x : G H) :
Monoid.Coprod.mk (FreeMonoid.of (Sum.map Inv.inv Inv.inv x)) * Monoid.Coprod.mk () = 1
theorem AddMonoid.Coprod.con_add_left_neg {G : Type u_1} {H : Type u_2} [] [] (x : FreeAddMonoid (G H)) :
theorem Monoid.Coprod.con_mul_left_inv {G : Type u_1} {H : Type u_2} [] [] (x : FreeMonoid (G H)) :
() (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList x)).reverse * x) 1
theorem AddMonoid.Coprod.instNeg.proof_1 {G : Type u_2} {H : Type u_1} [] [] :
instance AddMonoid.Coprod.instNeg {G : Type u_1} {H : Type u_2} [] [] :
Neg ()
Equations
• One or more equations did not get rendered due to their size.
instance Monoid.Coprod.instInv {G : Type u_1} {H : Type u_2} [] [] :
Inv ()
Equations
• One or more equations did not get rendered due to their size.
theorem AddMonoid.Coprod.neg_def {G : Type u_1} {H : Type u_2} [] [] (w : FreeAddMonoid (G H)) :
theorem Monoid.Coprod.inv_def {G : Type u_1} {H : Type u_2} [] [] (w : FreeMonoid (G H)) :
(Monoid.Coprod.mk w)⁻¹ = Monoid.Coprod.mk (FreeMonoid.ofList (List.map (Sum.map Inv.inv Inv.inv) (FreeMonoid.toList w)).reverse)
theorem AddMonoid.Coprod.instAddGroup.proof_5 {G : Type u_1} {H : Type u_2} [] [] (y : ) :
-y + y = 0
theorem AddMonoid.Coprod.instAddGroup.proof_1 {G : Type u_1} {H : Type u_2} [] [] :
∀ (a b : ), a - b = a - b
theorem AddMonoid.Coprod.instAddGroup.proof_4 {G : Type u_1} {H : Type u_2} [] [] :
∀ (n : ) (a : ), zsmulRec () a = zsmulRec () a
instance AddMonoid.Coprod.instAddGroup {G : Type u_1} {H : Type u_2} [] [] :
Equations
theorem AddMonoid.Coprod.instAddGroup.proof_2 {G : Type u_1} {H : Type u_2} [] [] :
∀ (a : ), zsmulRec 0 a = zsmulRec 0 a
theorem AddMonoid.Coprod.instAddGroup.proof_3 {G : Type u_1} {H : Type u_2} [] [] :
∀ (n : ) (a : ), zsmulRec (Int.ofNat n.succ) a = zsmulRec (Int.ofNat n.succ) a
instance Monoid.Coprod.instGroup {G : Type u_1} {H : Type u_2} [] [] :
Equations
• Monoid.Coprod.instGroup =
@[simp]
theorem AddMonoid.Coprod.closure_range_inl_union_inr {G : Type u_1} {H : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.closure_range_inl_union_inr {G : Type u_1} {H : Type u_2} [] [] :
Subgroup.closure (Set.range Monoid.Coprod.inl Set.range Monoid.Coprod.inr) =
@[simp]
theorem AddMonoid.Coprod.range_inl_sup_range_inr {G : Type u_1} {H : Type u_2} [] [] :
@[simp]
theorem Monoid.Coprod.range_inl_sup_range_inr {G : Type u_1} {H : Type u_2} [] [] :
Monoid.Coprod.inl.range Monoid.Coprod.inr.range =
theorem AddMonoid.Coprod.codisjoint_range_inl_range_inr {G : Type u_1} {H : Type u_2} [] [] :
theorem Monoid.Coprod.codisjoint_range_inl_range_inr {G : Type u_1} {H : Type u_2} [] [] :
Codisjoint Monoid.Coprod.inl.range Monoid.Coprod.inr.range
@[simp]
theorem AddMonoid.Coprod.range_swap {G : Type u_1} {H : Type u_2} [] [] :
().range =
@[simp]
theorem Monoid.Coprod.range_swap {G : Type u_1} {H : Type u_2} [] [] :
().range =
theorem AddMonoid.Coprod.range_eq {G : Type u_1} {H : Type u_2} [] [] {K : Type u_3} [] (f : →+ K) :
theorem Monoid.Coprod.range_eq {G : Type u_1} {H : Type u_2} [] [] {K : Type u_3} [] (f : →* K) :
f.range = (f.comp Monoid.Coprod.inl).range (f.comp Monoid.Coprod.inr).range
@[simp]
theorem AddMonoid.Coprod.range_lift {G : Type u_1} {H : Type u_2} [] [] {K : Type u_3} [] (f : G →+ K) (g : H →+ K) :
().range = f.range g.range
@[simp]
theorem Monoid.Coprod.range_lift {G : Type u_1} {H : Type u_2} [] [] {K : Type u_3} [] (f : G →* K) (g : H →* K) :
().range = f.range g.range
theorem AddMonoid.MulEquiv.coprodCongr.proof_3 {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoid.MulEquiv.coprodCongr.proof_2 {M' : Type u_1} {N' : Type u_2} [] [] :
AddMonoidHomClass (M' ≃+ N') M' N'
theorem AddMonoid.MulEquiv.coprodCongr.proof_1 {M : Type u_1} {N : Type u_2} [] [] :
theorem AddMonoid.MulEquiv.coprodCongr.proof_4 {M' : Type u_1} {N' : Type u_2} [] [] :
AddMonoidHomClass (N' ≃+ M') N' M'
theorem AddMonoid.MulEquiv.coprodCongr.proof_5 {M : Type u_1} {N : Type u_3} {M' : Type u_2} {N' : Type u_4} [] [] [] [] (e : M ≃+ N) (e' : M' ≃+ N') :
theorem AddMonoid.MulEquiv.coprodCongr.proof_6 {M : Type u_3} {N : Type u_1} {M' : Type u_4} {N' : Type u_2} [] [] [] [] (e : M ≃+ N) (e' : M' ≃+ N') :
def AddMonoid.MulEquiv.coprodCongr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃+ N) (e' : M' ≃+ N') :

Lift two additive monoid equivalences e : M ≃+ N and e' : M' ≃+ N' to an additive monoid equivalence (AddMonoid.Coprod M M') ≃+ (AddMonoid.Coprod N N').

Equations
Instances For
@[simp]
theorem AddMonoid.MulEquiv.coprodCongr_symm_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃+ N) (e' : M' ≃+ N') :
@[simp]
theorem Monoid.MulEquiv.coprodCongr_symm_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃* N) (e' : M' ≃* N') :
().symm = (Monoid.Coprod.map e.symm e'.symm)
@[simp]
theorem Monoid.MulEquiv.coprodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃* N) (e' : M' ≃* N') :
() = (Monoid.Coprod.map e e')
@[simp]
theorem AddMonoid.MulEquiv.coprodCongr_apply {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃+ N) (e' : M' ≃+ N') :
def Monoid.MulEquiv.coprodCongr {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [] [] [] [] (e : M ≃* N) (e' : M' ≃* N') :

Lift two monoid equivalences e : M ≃* N and e' : M' ≃* N' to a monoid equivalence (M ∗ M') ≃* (N ∗ N').

Equations
Instances For
def AddMonoid.MulEquiv.coprodComm (M : Type u_1) (N : Type u_2) [] [] :

An AddEquiv version of AddMonoid.Coprod.swap.

Equations
Instances For
@[simp]
theorem Monoid.MulEquiv.coprodComm_symm_apply (M : Type u_1) (N : Type u_2) [] [] :
.symm = ()
@[simp]
theorem AddMonoid.MulEquiv.coprodComm_symm_apply (M : Type u_1) (N : Type u_2) [] [] :
.symm = ()
@[simp]
theorem AddMonoid.MulEquiv.coprodComm_apply (M : Type u_1) (N : Type u_2) [] [] :
= ()
@[simp]
theorem Monoid.MulEquiv.coprodComm_apply (M : Type u_1) (N : Type u_2) [] [] :
= ()
def Monoid.MulEquiv.coprodComm (M : Type u_1) (N : Type u_2) [] [] :

A MulEquiv version of Coprod.swap.

Equations
• = ().toMulEquiv ()
Instances For
theorem AddMonoid.MulEquiv.coprodAssoc.proof_1 (M : Type u_1) (N : Type u_2) (P : Type u_3) [] [] [] :
def AddMonoid.MulEquiv.coprodAssoc (M : Type u_1) (N : Type u_2) (P : Type u_3) [] [] [] :

An additive equivalence between AddMonoid.Coprod (AddMonoid.Coprod M N) P and AddMonoid.Coprod M (AddMonoid.Coprod N P).

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem AddMonoid.MulEquiv.coprodAssoc.proof_2 (M : Type u_1) (N : Type u_2) (P : Type u_3) [] [] [] :
def Monoid.MulEquiv.coprodAssoc (M : Type u_1) (N : Type u_2) (P : Type u_3) [] [] [] :

A multiplicative equivalence between (M ∗ N) ∗ P and M ∗ (N ∗ P).

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_apply_inl_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : M) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : M) :
() (Monoid.Coprod.inl (Monoid.Coprod.inl x)) = Monoid.Coprod.inl x
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_apply_inl_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : N) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_apply_inl_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : N) :
() (Monoid.Coprod.inl (Monoid.Coprod.inr x)) = Monoid.Coprod.inr (Monoid.Coprod.inl x)
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : P) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_apply_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : P) :
() (Monoid.Coprod.inr x) = Monoid.Coprod.inr (Monoid.Coprod.inr x)
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : M) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : M) :
().symm (Monoid.Coprod.inl x) = Monoid.Coprod.inl (Monoid.Coprod.inl x)
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inr_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : N) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inl {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : N) :
().symm (Monoid.Coprod.inr (Monoid.Coprod.inl x)) = Monoid.Coprod.inl (Monoid.Coprod.inr x)
@[simp]
theorem AddMonoid.MulEquiv.coprodAssoc_symm_apply_inr_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : P) :
@[simp]
theorem Monoid.MulEquiv.coprodAssoc_symm_apply_inr_inr {M : Type u_1} {N : Type u_2} {P : Type u_3} [] [] [] (x : P) :
().symm (Monoid.Coprod.inr (Monoid.Coprod.inr x)) = Monoid.Coprod.inr x
@[simp]
theorem Monoid.MulEquiv.coprodPUnit_apply (M : Type u_1) [] :
= Monoid.Coprod.fst
@[simp]
theorem Monoid.MulEquiv.coprodPUnit_symm_apply (M : Type u_1) [] :
.symm = Monoid.Coprod.inl

Isomorphism between M ∗ PUnit and M.

Equations
• = Monoid.Coprod.fst.toMulEquiv Monoid.Coprod.inl
Instances For
@[simp]
theorem Monoid.MulEquiv.punitCoprod_apply (M : Type u_1) [] :
= Monoid.Coprod.snd
@[simp]
theorem Monoid.MulEquiv.punitCoprod_symm_apply (M : Type u_1) [] :
.symm = Monoid.Coprod.inr

Isomorphism between PUnit ∗ M and M.

Equations
• = Monoid.Coprod.snd.toMulEquiv Monoid.Coprod.inr
Instances For
@[simp]
theorem Monoid.AddEquiv.coprodUnit_apply {M : Type u_1} [] :
@[simp]
theorem Monoid.AddEquiv.coprodUnit_symm_apply {M : Type u_1} [] :
def Monoid.AddEquiv.coprodUnit {M : Type u_1} [] :

Isomorphism between M ∗ PUnit and M.

Equations
Isomorphism between PUnit ∗ M and M.