length_mul — Mathlib

English

Let x and y be elements of the free semigroup on α. The length of their product is the sum of their lengths: |x · y| = |x| + |y|.

Русский

Пусть x и y — элементы свободной полугруппы над α. Длина их произведения равна сумме длин: |x · y| = |x| + |y|.

LaTeX

$$$|x \cdot y| = |x| + |y|$$$

Lean4

@[to_additive (attr := simp)]
theorem length_mul (x y : FreeSemigroup α) : (x * y).length = x.length + y.length := by
  simp [length, Nat.add_right_comm, List.length, List.length_append]

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