Nat.Partition.parts_sum
theorem Nat.Partition.parts_sum : ∀ {n : ℕ} (self : n.Partition), self.parts.sum = n
This theorem states that for any natural number `n` and any partition `self` of `n`, the sum of the `parts` of the partition is equal to `n`. In other words, if you take a natural number and partition it into a set of smaller natural numbers, the sum of these smaller numbers will always equal the original number. This is a fundamental property of number partitions.
More concisely: For any natural number `n` and its partition `self`, the sum of the parts of `self` equals `n`.
|
Nat.Partition.parts_pos
theorem Nat.Partition.parts_pos : ∀ {n : ℕ} (self : n.Partition) {i : ℕ}, i ∈ self.parts → 0 < i
This theorem proves that all `parts` of a natural number partition are positive. Given a natural number `n` and a partition `self` of `n`, the theorem asserts that for any natural number `i`, if `i` is in the list of `parts` of the partition, then `i` must be greater than zero.
More concisely: Given a natural number partition `self` of a natural number `n`, all parts of the partition are positive (i.e., greater than zero).
|
Nat.Partition.ext
theorem Nat.Partition.ext : ∀ {n : ℕ} (x y : n.Partition), x.parts = y.parts → x = y
This theorem, `Nat.Partition.ext`, states that for any natural number `n` and any two partitions `x` and `y` of `n`, if the parts of `x` and `y` are equal, then `x` and `y` are equal. In simpler terms, it ensures that two partitions of a natural number are considered the same if they have the same parts, regardless of the order in which these parts are supplied.
More concisely: If two partitions of a natural number have equal parts, then they are equal.
|
Nat.Partition.count_ofSums_of_ne_zero
theorem Nat.Partition.count_ofSums_of_ne_zero :
∀ {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n) {i : ℕ},
i ≠ 0 → Multiset.count i (Nat.Partition.ofSums n l hl).parts = Multiset.count i l
The theorem `Nat.Partition.count_ofSums_of_ne_zero` states that for any positive integer `i`, the number of times `i` appears in the partition of a number `n` obtained from the multiset `l` whose sum is `n`, is the same as the number of times `i` appears in the original multiset `l`. This only holds true when `i` is not zero. If `i` is zero, then by virtue of partitions not containing zeros and by the property that a multiset count of a non-member is zero, the count in both the partition and the multiset would be zero.
More concisely: For a positive integer `i`, the number of occurrences of `i` in the partition of a multiset `l` with sum `n` equals the multiset count of `i` in `l`, provided `i` is non-zero.
|