length_reverse

Mathlib.Algebra.FreeMonoid.Basic

URI: https://scilib.ai/kg/mathlib#FreeMonoid.length_reverse

English

Reversing preserves length: length of a.reverse equals length of a.

Русский

Длина сохраняется при развороте: length(а.reverse) = length(а).

LaTeX

$$$ a.reverse.length = a.length $$$

Lean4

@[to_additive (attr := simp)]
theorem length_reverse {a : FreeMonoid α} : a.reverse.length = a.length :=
  List.length_reverse

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru