mathlib documentation

algebra.free

Free constructions

Main definitions

source
inductive free_magma (α : Type u) :
Type u

Free magma over a given alphabet.

source
@[instance]
def free_magma.decidable_eq (α : Type u) [a : decidable_eq α] :
decidable_eq (free_magma α)

source
@[instance]
def free_add_magma.decidable_eq (α : Type u) [a : decidable_eq α] :
decidable_eq (free_add_magma α)

source
inductive free_add_magma (α : Type u) :
Type u

Free nonabelian additive magma over a given alphabet.

source
@[instance]
def free_add_magma.inhabited {α : Type u} [inhabited α] :
inhabited (free_add_magma α)

source
@[instance]
def free_magma.inhabited {α : Type u} [inhabited α] :
inhabited (free_magma α)

Equations
source
@[instance]
def free_add_magma.has_add {α : Type u} :
has_add (free_add_magma α)

source
@[instance]
def free_magma.has_mul {α : Type u} :
has_mul (free_magma α)

Equations
source
@[simp]
theorem free_magma.mul_eq {α : Type u} (x y : free_magma α) :
x.mul y = x * y

source
@[simp]
theorem free_add_magma.add_eq {α : Type u} (x y : free_add_magma α) :
x.add y = x + y

source
def free_magma.rec_on' {α : Type u} {C : free_magma α → Sort l} (x : free_magma α) (ih1 : Π (x : α), C (free_magma.of x)) (ih2 : Π (x y : free_magma α), C x → C y → C (x * y)) :
C x

Recursor for free_magma using x * y instead of free_magma.mul x y.

Equations
source
def free_add_magma.rec_on' {α : Type u} {C : free_add_magma α → Sort l} (x : free_add_magma α) (ih1 : Π (x : α), C (free_add_magma.of x)) (ih2 : Π (x y : free_add_magma α), C x → C y → C (x + y)) :
C x

Recursor for free_add_magma using x + y instead of free_add_magma.add x y.

source
def free_magma.lift {α : Type u} {β : Type v} [has_mul β] (f : α → β) (a : free_magma α) :
β

Lifts a function α → β to a magma homomorphism free_magma α → β given a magma β.

Equations
source
def free_add_magma.lift {α : Type u} {β : Type v} [has_add β] (f : α → β) (a : free_add_magma α) :
β

Lifts a function α → β to an additive magma homomorphism free_add_magma α → β given an additive magma β.

Equations
source
@[simp]
theorem free_add_magma.lift_of {α : Type u} {β : Type v} [has_add β] (f : α → β) (x : α) :
free_add_magma.lift f (free_add_magma.of x) = f x

source
@[simp]
theorem free_magma.lift_of {α : Type u} {β : Type v} [has_mul β] (f : α → β) (x : α) :
free_magma.lift f (free_magma.of x) = f x

source
@[simp]
theorem free_magma.lift_mul {α : Type u} {β : Type v} [has_mul β] (f : α → β) (x y : free_magma α) :
free_magma.lift f (x * y) = (free_magma.lift f x) * free_magma.lift f y

source
@[simp]
theorem free_add_magma.lift_add {α : Type u} {β : Type v} [has_add β] (f : α → β) (x y : free_add_magma α) :
free_add_magma.lift f (x + y) = free_add_magma.lift f x + free_add_magma.lift f y

source
theorem free_magma.lift_unique {α : Type u} {β : Type v} [has_mul β] (f : free_magma α → β) (hf : ∀ (x y : free_magma α), f (x * y) = (f x) * f y) :
f = free_magma.lift (f ∘ free_magma.of)

source
theorem free_add_magma.lift_unique {α : Type u} {β : Type v} [has_add β] (f : free_add_magma α → β) (hf : ∀ (x y : free_add_magma α), f (x + y) = f x + f y) :
f = free_add_magma.lift (f ∘ free_add_magma.of)

source
def free_magma.map {α : Type u} {β : Type v} (f : α → β) (a : free_magma α) :
free_magma β

The unique magma homomorphism free_magma α → free_magma β that sends each of x to of (f x).

Equations
source
def free_add_magma.map {α : Type u} {β : Type v} (f : α → β) (a : free_add_magma α) :
free_add_magma β

The unique additive magma homomorphism free_add_magma α → free_add_magma β that sends each of x to of (f x).

Equations
source
@[simp]
theorem free_add_magma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :
free_add_magma.map f (free_add_magma.of x) = free_add_magma.of (f x)

source
@[simp]
theorem free_magma.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :
free_magma.map f (free_magma.of x) = free_magma.of (f x)

source
@[simp]
theorem free_add_magma.map_add {α : Type u} {β : Type v} (f : α → β) (x y : free_add_magma α) :
free_add_magma.map f (x + y) = free_add_magma.map f x + free_add_magma.map f y

source
@[simp]
theorem free_magma.map_mul {α : Type u} {β : Type v} (f : α → β) (x y : free_magma α) :
free_magma.map f (x * y) = (free_magma.map f x) * free_magma.map f y

source
@[instance]
def free_add_magma.monad  :
monad free_add_magma

source
@[instance]
def free_magma.monad  :
monad free_magma

Equations
source
def free_magma.rec_on'' {α : Type u} {C : free_magma α → Sort l} (x : free_magma α) (ih1 : Π (x : α), C (pure x)) (ih2 : Π (x y : free_magma α), C x → C y → C (x * y)) :
C x

Recursor on free_magma using pure instead of of.

Equations
source
def free_add_magma.rec_on'' {α : Type u} {C : free_add_magma α → Sort l} (x : free_add_magma α) (ih1 : Π (x : α), C (pure x)) (ih2 : Π (x y : free_add_magma α), C x → C y → C (x + y)) :
C x

Recursor on free_add_magma using pure instead of of.

source
@[simp]
theorem free_magma.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)

source
@[simp]
theorem free_add_magma.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)

source
@[simp]
theorem free_magma.map_mul' {α β : Type u} (f : α → β) (x y : free_magma α) :
f <$> x * y = (f <$> x) * f <$> y

source
@[simp]
theorem free_add_magma.map_add' {α β : Type u} (f : α → β) (x y : free_add_magma α) :
f <$> (x + y) = f <$> x + f <$> y

source
@[simp]
theorem free_add_magma.pure_bind {α β : Type u} (f : α → free_add_magma β) (x : α) :
pure x >>= f = f x

source
@[simp]
theorem free_magma.pure_bind {α β : Type u} (f : α → free_magma β) (x : α) :
pure x >>= f = f x

source
@[simp]
theorem free_add_magma.add_bind {α β : Type u} (f : α → free_add_magma β) (x y : free_add_magma α) :
x + y >>= f = (x >>= f) + (y >>= f)

source
@[simp]
theorem free_magma.mul_bind {α β : Type u} (f : α → free_magma β) (x y : free_magma α) :
x * y >>= f = (x >>= f) * (y >>= f)

source
@[simp]
theorem free_add_magma.pure_seq {α β : Type u} {f : α → β} {x : free_add_magma α} :
pure f <*> x = f <$> x

source
@[simp]
theorem free_magma.pure_seq {α β : Type u} {f : α → β} {x : free_magma α} :
pure f <*> x = f <$> x

source
@[simp]
theorem free_add_magma.add_seq {α β : Type u} {f g : free_add_magma (α → β)} {x : free_add_magma α} :
f + g <*> x = (f <*> x) + (g <*> x)

source
@[simp]
theorem free_magma.mul_seq {α β : Type u} {f g : free_magma (α → β)} {x : free_magma α} :
f * g <*> x = (f <*> x) * (g <*> x)

source
@[instance]
def free_add_magma.is_lawful_monad  :
is_lawful_monad free_add_magma

source
@[instance]
def free_magma.is_lawful_monad  :
is_lawful_monad free_magma

source
def free_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (a : free_magma α) :
m (free_magma β)

free_magma is traversable.

Equations
source
def free_add_magma.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (a : free_add_magma α) :
m (free_add_magma β)

free_add_magma is traversable.

Equations
source
@[instance]
def free_magma.traversable  :
traversable free_magma

Equations
source
@[instance]
def free_add_magma.traversable  :
traversable free_add_magma

source
@[simp]
theorem free_magma.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :
traverse F (pure x) = pure <$> F x

source
@[simp]
theorem free_add_magma.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :
traverse F (pure x) = pure <$> F x

source
@[simp]
theorem free_add_magma.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
traverse F ∘ pure = λ (x : α), pure <$> F x

source
@[simp]
theorem free_magma.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
traverse F ∘ pure = λ (x : α), pure <$> F x

source
@[simp]
theorem free_add_magma.traverse_add {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x y : free_add_magma α) :
traverse F (x + y) = has_add.add <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_magma.traverse_mul {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x y : free_magma α) :
traverse F (x * y) = has_mul.mul <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_magma.traverse_mul' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
function.comp (traverse F) ∘ has_mul.mul = λ (x y : free_magma α), has_mul.mul <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_add_magma.traverse_add' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
function.comp (traverse F) ∘ has_add.add = λ (x y : free_add_magma α), has_add.add <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_magma.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_magma α) :
free_magma.traverse F x = traverse F x

source
@[simp]
theorem free_add_magma.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_add_magma α) :
free_add_magma.traverse F x = traverse F x

source
@[simp]
theorem free_add_magma.add_map_seq {α : Type u} (x y : free_add_magma α) :
has_add.add <$> x <*> y = x + y

source
@[simp]
theorem free_magma.mul_map_seq {α : Type u} (x y : free_magma α) :
has_mul.mul <$> x <*> y = x * y

source
@[instance]
def free_magma.is_lawful_traversable  :
is_lawful_traversable free_magma

Equations
source
@[instance]
def free_add_magma.is_lawful_traversable  :
is_lawful_traversable free_add_magma

source
def free_magma.repr {α : Type u} [has_repr α] (a : free_magma α) :
string

Representation of an element of a free magma.

Equations
source
def free_add_magma.repr {α : Type u} [has_repr α] (a : free_add_magma α) :
string

Representation of an element of a free additive magma.

Equations
source
@[instance]
def free_magma.has_repr {α : Type u} [has_repr α] :
has_repr (free_magma α)

Equations
source
@[instance]
def free_add_magma.has_repr {α : Type u} [has_repr α] :
has_repr (free_add_magma α)

source
def free_magma.length {α : Type u} (a : free_magma α) :
ℕ

Length of an element of a free magma.

Equations
source
def free_add_magma.length {α : Type u} (a : free_add_magma α) :
ℕ

Length of an element of a free additive magma.

Equations
source
inductive magma.free_semigroup.r (α : Type u) [has_mul α] (a a_1 : α) :
Prop

Associativity relations for a magma.

source
inductive add_magma.free_add_semigroup.r (α : Type u) [has_add α] (a a_1 : α) :
Prop

Associativity relations for an additive magma.

source
def magma.free_semigroup (α : Type u) [has_mul α] :
Type u

Free semigroup over a magma.

Equations
source
def add_magma.free_add_semigroup (α : Type u) [has_add α] :
Type u

Free additive semigroup over an additive magma.

source
def magma.free_semigroup.of {α : Type u} [has_mul α] (a : α) :
magma.free_semigroup α

Embedding from magma to its free semigroup.

Equations
source
def add_magma.free_add_semigroup.of {α : Type u} [has_add α] (a : α) :
add_magma.free_add_semigroup α

Embedding from additive magma to its free additive semigroup.

source
@[instance]
def magma.free_semigroup.inhabited {α : Type u} [has_mul α] [inhabited α] :
inhabited (magma.free_semigroup α)

Equations
source
@[instance]
def add_magma.free_add_semigroup.inhabited {α : Type u} [has_add α] [inhabited α] :
inhabited (add_magma.free_add_semigroup α)

source
theorem add_magma.free_add_semigroup.induction_on {α : Type u} [has_add α] {C : add_magma.free_add_semigroup α → Prop} (x : add_magma.free_add_semigroup α) (ih : ∀ (x : α), C (add_magma.free_add_semigroup.of x)) :
C x

source
theorem magma.free_semigroup.induction_on {α : Type u} [has_mul α] {C : magma.free_semigroup α → Prop} (x : magma.free_semigroup α) (ih : ∀ (x : α), C (magma.free_semigroup.of x)) :
C x

source
theorem magma.free_semigroup.of_mul_assoc {α : Type u} [has_mul α] (x y z : α) :
magma.free_semigroup.of ((x * y) * z) = magma.free_semigroup.of (x * y * z)

source
theorem add_magma.free_add_semigroup.of_add_assoc {α : Type u} [has_add α] (x y z : α) :
add_magma.free_add_semigroup.of (x + y + z) = add_magma.free_add_semigroup.of (x + (y + z))

source
theorem add_magma.free_add_semigroup.of_add_assoc_left {α : Type u} [has_add α] (w x y z : α) :
add_magma.free_add_semigroup.of (w + (x + y + z)) = add_magma.free_add_semigroup.of (w + (x + (y + z)))

source
theorem magma.free_semigroup.of_mul_assoc_left {α : Type u} [has_mul α] (w x y z : α) :
magma.free_semigroup.of (w * (x * y) * z) = magma.free_semigroup.of (w * x * y * z)

source
theorem add_magma.free_add_semigroup.of_add_assoc_right {α : Type u} [has_add α] (w x y z : α) :
add_magma.free_add_semigroup.of (w + x + y + z) = add_magma.free_add_semigroup.of (w + (x + y) + z)

source
theorem magma.free_semigroup.of_mul_assoc_right {α : Type u} [has_mul α] (w x y z : α) :
magma.free_semigroup.of (((w * x) * y) * z) = magma.free_semigroup.of ((w * x * y) * z)

source
@[instance]
def add_magma.free_add_semigroup.add_semigroup {α : Type u} [has_add α] :
add_semigroup (add_magma.free_add_semigroup α)

source
@[instance]
def magma.free_semigroup.semigroup {α : Type u} [has_mul α] :
semigroup (magma.free_semigroup α)

Equations
source
theorem magma.free_semigroup.of_mul {α : Type u} [has_mul α] (x y : α) :
magma.free_semigroup.of (x * y) = (magma.free_semigroup.of x) * magma.free_semigroup.of y

source
theorem add_magma.free_add_semigroup.of_add {α : Type u} [has_add α] (x y : α) :
add_magma.free_add_semigroup.of (x + y) = add_magma.free_add_semigroup.of x + add_magma.free_add_semigroup.of y

source
def magma.free_semigroup.lift {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α → β) (hf : ∀ (x y : α), f (x * y) = (f x) * f y) (a : magma.free_semigroup α) :
β

Lifts a magma homomorphism α → β to a semigroup homomorphism magma.free_semigroup α → β given a semigroup β.

Equations
source
def add_magma.free_add_semigroup.lift {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : α → β) (hf : ∀ (x y : α), f (x + y) = f x + f y) (a : add_magma.free_add_semigroup α) :
β

Lifts an additive magma homomorphism α → β to an additive semigroup homomorphism add_magma.free_add_semigroup α → β given an additive semigroup β.

source
@[simp]
theorem magma.free_semigroup.lift_of {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α → β) {hf : ∀ (x y : α), f (x * y) = (f x) * f y} (x : α) :
magma.free_semigroup.lift f hf (magma.free_semigroup.of x) = f x

source
@[simp]
theorem add_magma.free_add_semigroup.lift_of {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : α → β) {hf : ∀ (x y : α), f (x + y) = f x + f y} (x : α) :
add_magma.free_add_semigroup.lift f hf (add_magma.free_add_semigroup.of x) = f x

source
@[simp]
theorem add_magma.free_add_semigroup.lift_add {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : α → β) {hf : ∀ (x y : α), f (x + y) = f x + f y} (x y : add_magma.free_add_semigroup α) :
add_magma.free_add_semigroup.lift f hf (x + y) = add_magma.free_add_semigroup.lift f hf x + add_magma.free_add_semigroup.lift f hf y

source
@[simp]
theorem magma.free_semigroup.lift_mul {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : α → β) {hf : ∀ (x y : α), f (x * y) = (f x) * f y} (x y : magma.free_semigroup α) :
magma.free_semigroup.lift f hf (x * y) = (magma.free_semigroup.lift f hf x) * magma.free_semigroup.lift f hf y

source
theorem add_magma.free_add_semigroup.lift_unique {α : Type u} [has_add α] {β : Type v} [add_semigroup β] (f : add_magma.free_add_semigroup α → β) (hf : ∀ (x y : add_magma.free_add_semigroup α), f (x + y) = f x + f y) :
f = add_magma.free_add_semigroup.lift (f ∘ add_magma.free_add_semigroup.of) _

source
theorem magma.free_semigroup.lift_unique {α : Type u} [has_mul α] {β : Type v} [semigroup β] (f : magma.free_semigroup α → β) (hf : ∀ (x y : magma.free_semigroup α), f (x * y) = (f x) * f y) :
f = magma.free_semigroup.lift (f ∘ magma.free_semigroup.of) _

source
def add_magma.free_add_semigroup.map {α : Type u} [has_add α] {β : Type v} [has_add β] (f : α → β) (hf : ∀ (x y : α), f (x + y) = f x + f y) (a : add_magma.free_add_semigroup α) :
add_magma.free_add_semigroup β

From an additive magma homomorphism α → β to an additive semigroup homomorphism add_magma.free_add_semigroup α → add_magma.free_add_semigroup β.

source
def magma.free_semigroup.map {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α → β) (hf : ∀ (x y : α), f (x * y) = (f x) * f y) (a : magma.free_semigroup α) :
magma.free_semigroup β

From a magma homomorphism α → β to a semigroup homomorphism magma.free_semigroup α → magma.free_semigroup β.

Equations
source
@[simp]
theorem add_magma.free_add_semigroup.map_of {α : Type u} [has_add α] {β : Type v} [has_add β] (f : α → β) {hf : ∀ (x y : α), f (x + y) = f x + f y} (x : α) :
add_magma.free_add_semigroup.map f hf (add_magma.free_add_semigroup.of x) = add_magma.free_add_semigroup.of (f x)

source
@[simp]
theorem magma.free_semigroup.map_of {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α → β) {hf : ∀ (x y : α), f (x * y) = (f x) * f y} (x : α) :
magma.free_semigroup.map f hf (magma.free_semigroup.of x) = magma.free_semigroup.of (f x)

source
@[simp]
theorem add_magma.free_add_semigroup.map_add {α : Type u} [has_add α] {β : Type v} [has_add β] (f : α → β) {hf : ∀ (x y : α), f (x + y) = f x + f y} (x y : add_magma.free_add_semigroup α) :
add_magma.free_add_semigroup.map f hf (x + y) = add_magma.free_add_semigroup.map f hf x + add_magma.free_add_semigroup.map f hf y

source
@[simp]
theorem magma.free_semigroup.map_mul {α : Type u} [has_mul α] {β : Type v} [has_mul β] (f : α → β) {hf : ∀ (x y : α), f (x * y) = (f x) * f y} (x y : magma.free_semigroup α) :
magma.free_semigroup.map f hf (x * y) = (magma.free_semigroup.map f hf x) * magma.free_semigroup.map f hf y

source
def free_add_semigroup (α : Type u) :
Type u

Free additive semigroup over a given alphabet.

source
def free_semigroup (α : Type u) :
Type u

Free semigroup over a given alphabet. (Note: In this definition, the free semigroup does not contain the empty word.)

Equations
source
@[instance]
def free_semigroup.semigroup {α : Type u} :
semigroup (free_semigroup α)

Equations
source
@[instance]
def free_add_semigroup.add_semigroup {α : Type u} :
add_semigroup (free_add_semigroup α)

source
def free_semigroup.of {α : Type u} (x : α) :
free_semigroup α

The embedding α → free_semigroup α.

Equations
source
def free_add_semigroup.of {α : Type u} (x : α) :
free_add_semigroup α

The embedding α → free_add_semigroup α.

source
@[instance]
def free_add_semigroup.inhabited {α : Type u} [inhabited α] :
inhabited (free_add_semigroup α)

source
@[instance]
def free_semigroup.inhabited {α : Type u} [inhabited α] :
inhabited (free_semigroup α)

Equations
source
def free_add_semigroup.rec_on {α : Type u} {C : free_add_semigroup α → Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), C (free_add_semigroup.of x)) (ih2 : Π (x : α) (y : free_add_semigroup α), C (free_add_semigroup.of x) → C y → C (free_add_semigroup.of x + y)) :
C x

Recursor for free additive semigroup using of and +.

source
def free_semigroup.rec_on {α : Type u} {C : free_semigroup α → Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C (free_semigroup.of x)) (ih2 : Π (x : α) (y : free_semigroup α), C (free_semigroup.of x) → C y → C ((free_semigroup.of x) * y)) :
C x

Recursor for free semigroup using of and *.

Equations
  • x.rec_on ih1 ih2 = prod.rec_on x (λ (f : α) (s : list α), s.rec_on ih1 (λ (hd : α) (tl : list α) (ih : Π (_a : α), C (_a, tl)) (f : α), ih2 f (hd, tl) (ih1 f) (ih hd)) f)
source
def free_semigroup.lift' {α : Type u} {β : Type v} [semigroup β] (f : α → β) (a : α) (a_1 : list α) :
β

Auxiliary function for free_semigroup.lift.

Equations
source
def free_add_semigroup.lift' {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (a : α) (a_1 : list α) :
β

Auxiliary function for free_semigroup.lift.

Equations
source
def free_semigroup.lift {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x : free_semigroup α) :
β

Lifts a function α → β to a semigroup homomorphism free_semigroup α → β given a semigroup β.

Equations
source
def free_add_semigroup.lift {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x : free_add_semigroup α) :
β

Lifts a function α → β to an additive semigroup homomorphism free_add_semigroup α → β given an additive semigroup β.

source
@[simp]
theorem free_semigroup.lift_of {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x : α) :
free_semigroup.lift f (free_semigroup.of x) = f x

source
@[simp]
theorem free_add_semigroup.lift_of {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x : α) :
free_add_semigroup.lift f (free_add_semigroup.of x) = f x

source
theorem free_add_semigroup.lift_of_add {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x : α) (y : free_add_semigroup α) :
free_add_semigroup.lift f (free_add_semigroup.of x + y) = f x + free_add_semigroup.lift f y

source
theorem free_semigroup.lift_of_mul {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x : α) (y : free_semigroup α) :
free_semigroup.lift f ((free_semigroup.of x) * y) = (f x) * free_semigroup.lift f y

source
@[simp]
theorem free_add_semigroup.lift_add {α : Type u} {β : Type v} [add_semigroup β] (f : α → β) (x y : free_add_semigroup α) :
free_add_semigroup.lift f (x + y) = free_add_semigroup.lift f x + free_add_semigroup.lift f y

source
@[simp]
theorem free_semigroup.lift_mul {α : Type u} {β : Type v} [semigroup β] (f : α → β) (x y : free_semigroup α) :
free_semigroup.lift f (x * y) = (free_semigroup.lift f x) * free_semigroup.lift f y

source
theorem free_add_semigroup.lift_unique {α : Type u} {β : Type v} [add_semigroup β] (f : free_add_semigroup α → β) (hf : ∀ (x y : free_add_semigroup α), f (x + y) = f x + f y) :
f = free_add_semigroup.lift (f ∘ free_add_semigroup.of)

source
theorem free_semigroup.lift_unique {α : Type u} {β : Type v} [semigroup β] (f : free_semigroup α → β) (hf : ∀ (x y : free_semigroup α), f (x * y) = (f x) * f y) :
f = free_semigroup.lift (f ∘ free_semigroup.of)

source
def free_semigroup.map {α : Type u} {β : Type v} (f : α → β) (a : free_semigroup α) :
free_semigroup β

The unique semigroup homomorphism that sends of x to of (f x).

Equations
source
def free_add_semigroup.map {α : Type u} {β : Type v} (f : α → β) (a : free_add_semigroup α) :
free_add_semigroup β

The unique additive semigroup homomorphism that sends of x to of (f x).

source
@[simp]
theorem free_add_semigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :
free_add_semigroup.map f (free_add_semigroup.of x) = free_add_semigroup.of (f x)

source
@[simp]
theorem free_semigroup.map_of {α : Type u} {β : Type v} (f : α → β) (x : α) :
free_semigroup.map f (free_semigroup.of x) = free_semigroup.of (f x)

source
@[simp]
theorem free_add_semigroup.map_add {α : Type u} {β : Type v} (f : α → β) (x y : free_add_semigroup α) :
free_add_semigroup.map f (x + y) = free_add_semigroup.map f x + free_add_semigroup.map f y

source
@[simp]
theorem free_semigroup.map_mul {α : Type u} {β : Type v} (f : α → β) (x y : free_semigroup α) :
free_semigroup.map f (x * y) = (free_semigroup.map f x) * free_semigroup.map f y

source
@[instance]
def free_semigroup.monad  :
monad free_semigroup

Equations
source
@[instance]
def free_add_semigroup.monad  :
monad free_add_semigroup

source
def free_semigroup.rec_on' {α : Type u} {C : free_semigroup α → Sort l} (x : free_semigroup α) (ih1 : Π (x : α), C (pure x)) (ih2 : Π (x : α) (y : free_semigroup α), C (pure x) → C y → C ((pure x) * y)) :
C x

Recursor that uses pure instead of of.

Equations
source
def free_add_semigroup.rec_on' {α : Type u} {C : free_add_semigroup α → Sort l} (x : free_add_semigroup α) (ih1 : Π (x : α), C (pure x)) (ih2 : Π (x : α) (y : free_add_semigroup α), C (pure x) → C y → C (pure x + y)) :
C x

Recursor that uses pure instead of of.

source
@[simp]
theorem free_semigroup.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)

source
@[simp]
theorem free_add_semigroup.map_pure {α β : Type u} (f : α → β) (x : α) :
f <$> pure x = pure (f x)

source
@[simp]
theorem free_add_semigroup.map_add' {α β : Type u} (f : α → β) (x y : free_add_semigroup α) :
f <$> (x + y) = f <$> x + f <$> y

source
@[simp]
theorem free_semigroup.map_mul' {α β : Type u} (f : α → β) (x y : free_semigroup α) :
f <$> x * y = (f <$> x) * f <$> y

source
@[simp]
theorem free_add_semigroup.pure_bind {α β : Type u} (f : α → free_add_semigroup β) (x : α) :
pure x >>= f = f x

source
@[simp]
theorem free_semigroup.pure_bind {α β : Type u} (f : α → free_semigroup β) (x : α) :
pure x >>= f = f x

source
@[simp]
theorem free_add_semigroup.add_bind {α β : Type u} (f : α → free_add_semigroup β) (x y : free_add_semigroup α) :
x + y >>= f = (x >>= f) + (y >>= f)

source
@[simp]
theorem free_semigroup.mul_bind {α β : Type u} (f : α → free_semigroup β) (x y : free_semigroup α) :
x * y >>= f = (x >>= f) * (y >>= f)

source
@[simp]
theorem free_add_semigroup.pure_seq {α β : Type u} {f : α → β} {x : free_add_semigroup α} :
pure f <*> x = f <$> x

source
@[simp]
theorem free_semigroup.pure_seq {α β : Type u} {f : α → β} {x : free_semigroup α} :
pure f <*> x = f <$> x

source
@[simp]
theorem free_semigroup.mul_seq {α β : Type u} {f g : free_semigroup (α → β)} {x : free_semigroup α} :
f * g <*> x = (f <*> x) * (g <*> x)

source
@[simp]
theorem free_add_semigroup.add_seq {α β : Type u} {f g : free_add_semigroup (α → β)} {x : free_add_semigroup α} :
f + g <*> x = (f <*> x) + (g <*> x)

source
@[instance]
def free_semigroup.is_lawful_monad  :
is_lawful_monad free_semigroup

source
@[instance]
def free_add_semigroup.is_lawful_monad  :
is_lawful_monad free_add_semigroup

source
def free_add_semigroup.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (x : free_add_semigroup α) :
m (free_add_semigroup β)

free_add_semigroup is traversable.

source
def free_semigroup.traverse {m : Type u → Type u} [applicative m] {α β : Type u} (F : α → m β) (x : free_semigroup α) :
m (free_semigroup β)

free_semigroup is traversable.

Equations
source
@[instance]
def free_add_semigroup.traversable  :
traversable free_add_semigroup

source
@[instance]
def free_semigroup.traversable  :
traversable free_semigroup

Equations
source
@[simp]
theorem free_add_semigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :
traverse F (pure x) = pure <$> F x

source
@[simp]
theorem free_semigroup.traverse_pure {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : α) :
traverse F (pure x) = pure <$> F x

source
@[simp]
theorem free_add_semigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
traverse F ∘ pure = λ (x : α), pure <$> F x

source
@[simp]
theorem free_semigroup.traverse_pure' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) :
traverse F ∘ pure = λ (x : α), pure <$> F x

source
@[simp]
theorem free_add_semigroup.traverse_add {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] (x y : free_add_semigroup α) :
traverse F (x + y) = has_add.add <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_semigroup.traverse_mul {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] (x y : free_semigroup α) :
traverse F (x * y) = has_mul.mul <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_add_semigroup.traverse_add' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] :
function.comp (traverse F) ∘ has_add.add = λ (x y : free_add_semigroup α), has_add.add <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_semigroup.traverse_mul' {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) [is_lawful_applicative m] :
function.comp (traverse F) ∘ has_mul.mul = λ (x y : free_semigroup α), has_mul.mul <$> traverse F x <*> traverse F y

source
@[simp]
theorem free_semigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_semigroup α) :
free_semigroup.traverse F x = traverse F x

source
@[simp]
theorem free_add_semigroup.traverse_eq {α β : Type u} {m : Type u → Type u} [applicative m] (F : α → m β) (x : free_add_semigroup α) :
free_add_semigroup.traverse F x = traverse F x

source
@[simp]
theorem free_add_semigroup.add_map_seq {α : Type u} (x y : free_add_semigroup α) :
has_add.add <$> x <*> y = x + y

source
@[simp]
theorem free_semigroup.mul_map_seq {α : Type u} (x y : free_semigroup α) :
has_mul.mul <$> x <*> y = x * y

source
@[instance]
def free_add_semigroup.is_lawful_traversable  :
is_lawful_traversable free_add_semigroup

source
@[instance]
def free_semigroup.is_lawful_traversable  :
is_lawful_traversable free_semigroup

Equations
source
@[instance]
def free_add_semigroup.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (free_add_semigroup α)

source
@[instance]
def free_semigroup.decidable_eq {α : Type u} [decidable_eq α] :
decidable_eq (free_semigroup α)

Equations
source
def free_semigroup_free_magma (α : Type u) :
magma.free_semigroup (free_magma α) ≃ free_semigroup α

Isomorphism between magma.free_semigroup (free_magma α) and free_semigroup α.

Equations
source
def free_add_semigroup_free_add_magma (α : Type u) :
add_magma.free_add_semigroup (free_add_magma α) ≃ free_add_semigroup α

Isomorphism between add_magma.free_add_semigroup (free_add_magma α) and free_add_semigroup α.

source
@[simp]
theorem free_add_semigroup_free_add_magma_add {α : Type u} (x y : add_magma.free_add_semigroup (free_add_magma α)) :
⇑(free_add_semigroup_free_add_magma α) (x + y) = ⇑(free_add_semigroup_free_add_magma α) x + ⇑(free_add_semigroup_free_add_magma α) y

source
@[simp]
theorem free_semigroup_free_magma_mul {α : Type u} (x y : magma.free_semigroup (free_magma α)) :
⇑(free_semigroup_free_magma α) (x * y) = (⇑(free_semigroup_free_magma α) x) * ⇑(free_semigroup_free_magma α) y