blocks_eq_nil — Mathlib

English

Let c be a composition of n. Then its list of blocks is empty if and only if n = 0.

Русский

Пусть c — композиция числа n. Тогда список её блоков пуст тогда и только тогда, когда n = 0.

LaTeX

$$$c.blocks = [] \\iff n = 0$$$

Lean4

@[simp]
theorem blocks_eq_nil : c.blocks = [] ↔ n = 0 := by
  constructor
  · intro h
    simpa using congr(List.sum $h)
  · rintro rfl
    rw [← length_eq_zero_iff, ← nonpos_iff_eq_zero]
    exact c.length_le

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