ones_blocks

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.ones_blocks

English

The blocks of ones(n) are replicate n 1.

Русский

Блоки ones(n) равны replicate n 1.

LaTeX

$$$ (\\text{ones}(n)).blocks = \\text{replicate } n (1) $$$

Lean4

@[simp]
theorem ones_blocks (n : ℕ) : (ones n).blocks = replicate n (1 : ℕ) :=
  rfl

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

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

Разделы

Аффилиация

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