FreeMonoid.prodAux_eq
theorem FreeMonoid.prodAux_eq : ∀ {M : Type u_4} [inst : Monoid M] (l : List M), FreeMonoid.prodAux l = l.prod := by
sorry
The theorem `FreeMonoid.prodAux_eq` states that for any type `M` that forms a monoid, the function `FreeMonoid.prodAux` computes the same result as the function `List.prod` for any list `l` of elements from `M`. Essentially, it says that the product of elements in a list, calculated using `FreeMonoid.prodAux`, is identical to the product computed using `List.prod`. Both functions calculate the product by successively multiplying the elements of the list together, starting with the identity element for `FreeMonoid.prodAux` and the first element for `List.prod`.
More concisely: For any monoid `M` and list `l` of elements from `M`, `FreeMonoid.prodAux l` equals `List.prod l`.
|
FreeMonoid.hom_eq
theorem FreeMonoid.hom_eq :
∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] ⦃f g : FreeMonoid α →* M⦄,
(∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)) → f = g
The theorem `FreeMonoid.hom_eq` states that for any type `α` and any type `M` that has a monoid structure, if `f` and `g` are two monoid homomorphisms from the free monoid over `α` to `M` such that they map any singleton list generated from an element of `α` to the same element in `M`, then the two homomorphisms `f` and `g` are equal. In other words, any two monoid homomorphisms from the free monoid over a set `α` to another monoid `M` are determined uniquely by their action on the elements of `α`.
More concisely: Given a type `α` and a monoid `M`, any two monoid homomorphisms from the free monoid over `α` to `M` that agree on singleton lists are equal.
|
FreeAddMonoid.sumAux_eq
theorem FreeAddMonoid.sumAux_eq : ∀ {M : Type u_4} [inst : AddMonoid M] (l : List M), FreeAddMonoid.sumAux l = l.sum
The theorem `FreeAddMonoid.sumAux_eq` states that for any given type `M` which is an instance of `AddMonoid`, and any list `l` of elements from `M`, the result of applying the `FreeAddMonoid.sumAux` function to `l` is equal to the result of applying the `List.sum` function to `l`. In other words, these two functions, `FreeAddMonoid.sumAux` and `List.sum`, produce the same sum for any list of elements in an additive monoid.
More concisely: For any list `l` of elements in an additive monoid `M`, `FreeAddMonoid.sumAux l` equals `List.sum l`.
|
FreeAddMonoid.hom_eq
theorem FreeAddMonoid.hom_eq :
∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] ⦃f g : FreeAddMonoid α →+ M⦄,
(∀ (x : α), f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)) → f = g
This theorem, `FreeAddMonoid.hom_eq`, states that for any type `α` and another type `M` that is equipped with an addition operation (an additive monoid), given any two additive monoid homomorphisms `f` and `g` from `FreeAddMonoid α` to `M`, if `f` and `g` agree on the result when applied to any single element of `α` embedded into `FreeAddMonoid α` (i.e., `f (FreeAddMonoid.of x)` is equal to `g (FreeAddMonoid.of x)` for all `x` in `α`), then the two homomorphisms `f` and `g` are equal.
More concisely: If `f` and `g` are additive monoid homomorphisms from `FreeAddMonoid α` to an additive monoid `M` such that `f (FreeAddMonoid.of x) = g (FreeAddMonoid.of x)` for all `x` in `α`, then `f = g`.
|