The finite set of symbols in a FreeMonoid element #
This is separated from the main FreeMonoid file, as it imports the finiteness hierarchy
The set of unique symbols in an additive free monoid element
Equations
- a.symbols = List.toFinset a
Instances For
@[simp]
@[simp]
@[simp]
theorem
FreeAddMonoid.symbols_of
{α : Type u_1}
[DecidableEq α]
{m : α}
:
(FreeAddMonoid.of m).symbols = {m}
@[simp]
theorem
FreeMonoid.symbols_of
{α : Type u_1}
[DecidableEq α]
{m : α}
:
(FreeMonoid.of m).symbols = {m}
@[simp]
theorem
FreeAddMonoid.symbols_add
{α : Type u_1}
[DecidableEq α]
{a : FreeAddMonoid α}
{b : FreeAddMonoid α}
:
@[simp]
theorem
FreeMonoid.symbols_mul
{α : Type u_1}
[DecidableEq α]
{a : FreeMonoid α}
{b : FreeMonoid α}
:
@[simp]
@[simp]