ofList — Mathlib

English

The identity equivalence between List α and FreeMonoid α is given by Equiv.refl on both sides, i.e., FreeMonoid α ≃ List α with inverse ofList and toList as mutual inverses.

Русский

Идентичная эквивалентность между List α и FreeMonoid α задаётся через Equiv.refl, то есть FreeMonoid α ≃ List α с обратной связью ofList и toList как взаимно обратные.

LaTeX

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

Lean4

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

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