toList — Mathlib

English

There exists a canonical isomorphism between the free monoid on α and the list algebra List α, given by the identity equivalence.

Русский

Существует каноническое изоморождение свободного моноида на α и списка List α, задаваемое тождественным эквивалентом.

LaTeX

$$$ FreeMonoid\\,\\alpha \\cong List\\,\\alpha $$$

Lean4

/-- The identity equivalence between `FreeMonoid α` and `List α`. -/
@[to_additive /-- The identity equivalence between `FreeAddMonoid α` and `List α`. -/
    ]
def toList : FreeMonoid α ≃ List α :=
  Equiv.refl _

Похожие утверждения