instToString — Mathlib

English

Each composition is mapped to the string representation of its blocks; i.e., toString(c.blocks) is the string for c.

Русский

Каждая композиция кодируется строково через последовательность её блоков: toString(c.blocks).

LaTeX

$$$\\text{ToString}(\\mathrm{Composition}(n))\\;:\\; c \\mapsto \\mathrm{toString}(c.blocks)$$$

Lean4

instance (n : ℕ) : ToString (Composition n) :=
  ⟨fun c => toString c.blocks⟩

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