English
For a nonunital nonassociative semiring α, given a finite index set s and a function f: s → Holor α ds, if every f x has CP-rank at most n, then the sum over s of f x has CP-rank at most |s|·n.
Русский
Для ненулевого ассоциативного полугруппного кольца α: если для каждого x∈s выполнено CPRankMax n (f x), то CPRankMax (|s|·n) (∑ x∈s f x).
LaTeX
$$$$ (\\forall x \\in s, \\; CPRankMax n (f x)) \\rightarrow CPRankMax (s.card * n) (\\sum x ∈ s, f x) $$$$
Lean4
theorem cprankMax_sum [NonUnitalNonAssocSemiring α] {β} {n : ℕ} (s : Finset β) (f : β → Holor α ds) :
(∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (s.card * n) (∑ x ∈ s, f x) :=
letI := Classical.decEq β
Finset.induction_on s (by simp [CPRankMax.zero])
(by
intro x s (h_x_notin_s : x ∉ s) ih h_cprank
simp only [Finset.sum_insert h_x_notin_s, Finset.card_insert_of_notMem h_x_notin_s]
rw [Nat.right_distrib]
simp only [Nat.one_mul, Nat.add_comm]
have ih' : CPRankMax (Finset.card s * n) (∑ x ∈ s, f x) :=
by
apply ih
intro (x : β) (h_x_in_s : x ∈ s)
simp only [h_cprank, Finset.mem_insert_of_mem, h_x_in_s]
exact cprankMax_add (h_cprank x (Finset.mem_insert_self x s)) ih')
