reverse_eq_ones

Mathlib.Combinatorics.Enumerative.Composition

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

English

c.reverse equals ones n if and only if c equals ones n.

Русский

Разворот композиции равен единицам тогда и только тогда, когда сама композиция равна единицам.

LaTeX

$$$c.reverse = \\mathrm{ones}\\;n \\iff c = \\mathrm{ones}\\;n.$$$

Lean4

@[simp]
theorem reverse_eq_ones {c : Composition n} : c.reverse = ones n ↔ c = ones n :=
  reverse_injective.eq_iff' reverse_ones

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

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

Разделы

Аффилиация

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