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 α] :
          symbols 1 = ∅
          source
          @[simp]
          theorem FreeAddMonoid.symbols_zero {α : Type u_1} [DecidableEq α] :
          symbols 0 = ∅
          source
          @[simp]
          theorem FreeMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} :
          (of m).symbols = {m}
          source
          @[simp]
          theorem FreeAddMonoid.symbols_of {α : Type u_1} [DecidableEq α] {m : α} :
          (of m).symbols = {m}
          source
          @[simp]
          theorem FreeMonoid.symbols_mul {α : Type u_1} [DecidableEq α] {a b : FreeMonoid α} :
          (a * b).symbols = a.symbols ∪ b.symbols
          source
          @[simp]
          theorem FreeAddMonoid.symbols_add {α : Type u_1} [DecidableEq α] {a 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