length_of

Mathlib.Algebra.Free

URI: https://scilib.ai/kg/mathlib#FreeSemigroup.length_of

English

For any α, the element obtained by embedding x into the free semigroup (the generator) has length 1: |of(x)| = 1.

Русский

Пусть x произвольного типа α. Встроенный элемент of(x) имеет длину 1: |of(x)| = 1.

LaTeX

$$$|\text{of } x| = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem length_of (x : α) : (of x).length = 1 :=
  rfl

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

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

Разделы

Аффилиация

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