prod_singleton — Mathlib

English

The product of a singleton NeWord is the embedding of its head into the free product, i.e., (singleton x h).prod = of x.

Русский

Произведение одиночного NeWord — это внедрение головы в свободное произведение: (singleton x h).prod = of x.

LaTeX

$$$$\\text{singleton}(x,h).prod = \\operatorname{of}(x).$$$$

Lean4

@[simp]
theorem prod_singleton {i} (x : M i) (hne_one : x ≠ 1) : (singleton x hne_one).prod = of x := by
  simp [toWord, prod, Word.prod]

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