Documentation

Mathlib.Algebra.FreeMonoid.Symbols

The finite set of symbols in a FreeMonoid element #

This is separated from the main FreeMonoid file, as it imports the finiteness hierarchy

source
def FreeMonoid.symbols {α : Type u_1} [DecidableEq α] (a : FreeMonoid α) :
Finset α

the set of unique symbols in a free monoid element

Equations
Instances For
    source
    def FreeAddMonoid.symbols {α : Type u_1} [DecidableEq α] (a : FreeAddMonoid α) :
    Finset α

    The set of unique symbols in an additive free monoid element

    Equations
    Instances For
      source
      @[simp]
      theorem FreeMonoid.symbols_one {α : Type u_1} [DecidableEq α] :
      FreeMonoid.symbols 1 = ∅
      source
      @[simp]
      theorem FreeAddMonoid.symbols_zero {α : Type u_1} [DecidableEq α] :
      FreeAddMonoid.symbols 0 = ∅
      source
      @[simp]
      theorem FreeMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} :
      (FreeMonoid.of m).symbols = {m}
      source
      @[simp]
      theorem FreeAddMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} :
      (FreeAddMonoid.of m).symbols = {m}
      source
      @[simp]
      theorem FreeMonoid.symbols_mul {α : Type u_1} [DecidableEq α] {a : FreeMonoid α} {b : FreeMonoid α} :
      (a * b).symbols = a.symbols ∪ b.symbols
      source
      @[simp]
      theorem FreeAddMonoid.symbols_add {α : Type u_1} [DecidableEq α] {a : FreeAddMonoid α} {b : FreeAddMonoid α} :
      (a + b).symbols = a.symbols ∪ b.symbols
      source
      @[simp]
      theorem FreeMonoid.mem_symbols {α : Type u_1} [DecidableEq α] {m : α} {a : FreeMonoid α} :
      m ∈ a.symbols ↔ m ∈ a
      source
      @[simp]
      theorem FreeAddMonoid.mem_symbols {α : Type u_1} [DecidableEq α] {m : α} {a : FreeAddMonoid α} :
      m ∈ a.symbols ↔ m ∈ a