indiscrete_parts — Mathlib

English

Let n be a positive integer. The indiscrete partition of n has exactly one part, namely n.

Русский

Пусть n — положительное целое число. Разбиение indiscrete(n) состоит из одного блока размера n.

LaTeX

$$$n \ne 0 \Rightarrow \mathrm{parts}(\mathrm{indiscrete}(n)) = \{n\}$$$

Lean4

@[simp]
theorem indiscrete_parts {n : ℕ} (hn : n ≠ 0) : (indiscrete n).parts = { n } := by simp [indiscrete, filter_eq_self, hn]

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