length_toFreeSemigroup — Mathlib

English

The length is preserved by the coercion from FreeMagma to FreeSemigroup: length(toFreeSemigroup x) = x.length for any x ∈ FreeMagma α.

Русский

Длина сохраняется при переходе из FreeMagma в FreeSemigroup: length(toFreeSemigroup x) = x.length.

LaTeX

$$$\operatorname{length}(\text{toFreeSemigroup } x) = \operatorname{length}(x)$$$

Lean4

@[to_additive (attr := simp)]
theorem length_toFreeSemigroup (x : FreeMagma α) : (toFreeSemigroup x).length = x.length :=
  FreeMagma.recOnMul x (fun _ ↦ rfl) fun x y hx hy ↦ by rw [map_mul, FreeSemigroup.length_mul, hx, hy]; rfl

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