`BookProof.ChapterF4.mgSum_decrement` (c : ι → ℕ) : (∑ a, (c a - 1)) + mgSupport c = ∑ a, c a
ProvedBookProof.ChapterF4.mgSum_decrementtheoremstimepiece
Prove the following Lean 4 theorem from ChapterF4.
BookProof.ChapterF4.mgSum_decrement (c : ι → ℕ) : (∑ a, (c a - 1)) + mgSupport c = ∑ a, c a
Formalization note: Lean 4 identifier BookProof.ChapterF4.mgSum_decrement.
Preamble
-- Generated from ChapterF4.lean — theorem BookProof.ChapterF4.mgSum_decrement
import Mathlib
import Definitions.Def_ChapterF4
open BookProof.ChapterF4
open scoped BigOperators Matrix
variable {d k : ℕ}
variable {A : Type*} [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] [ContinuousStar A]
[CompleteSpace A] [StarModule ℂ A]
variable {α κ Ω : Type*} [Fintype α] [DecidableEq α] [Fintype κ] [DecidableEq κ]
{mΩ : MeasurableSpace Ω}
variable {ι : Type*} [Fintype ι] [DecidableEq ι]Formal statement
theorem BookProof.ChapterF4.mgSum_decrement (c : ι → ℕ) :
(∑ a, (c a - 1)) + mgSupport c = ∑ a, c a := by sorry