English
Let p = (head, tail) be a pair with head in M i and tail a word in M. Then the product of the word obtained by prepending the head to the tail equals the image of the head under the canonical embedding into the coproduct multiplied by the product of the tail: prod(rcons p) = of(p.head) · prod(p.tail).
Русский
Пусть p = (head, tail) — пара с head ∈ M i и tail — слово в M. Тогда произведение слова, полученного добавлением head в начало tail, равно образу head через каноническое встроение в копродикон, умноженному на произведение хвоста: prod(rcons p) = of(p.head) · prod(p.tail).
LaTeX
$$$\\operatorname{prod}(\\mathrm{rcons}(p)) = \\mathrm{of}(p.head) \\cdot \\operatorname{prod}(p.tail)$$$
Lean4
@[simp]
theorem prod_rcons {i} (p : Pair M i) : prod (rcons p) = of p.head * prod p.tail :=
if hm : p.head = 1 then by rw [rcons, dif_pos hm, hm, MonoidHom.map_one, one_mul]
else by rw [rcons, dif_neg hm, cons, prod, List.map_cons, List.prod_cons, prod]
