case pos
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)

case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
by_cases hf : Summable f
no goals
case pos
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
exact hf.hasSum.matrix_blockDiagonal.tsum_eq.symm
case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
have hft := summable_matrix_blockDiagonal.not.mpr hf
case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal 0 = 0
case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal (∑' (x : X), f x) = ∑' (x : X), blockDiagonal (f x)
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
no goals
case neg
X : Type u_5
α : Type ?u.94238
l : Type ?u.94241
m : Type u_3
n : Type u_4
p : Type u_1
S : Type ?u.94253
R : Type u_2
m' : l → Type ?u.94261
n' : l → Type ?u.94266
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq p
inst✝ : T2Space R
f : X → p → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => blockDiagonal (f x)
⊢ blockDiagonal 0 = 0
exact blockDiagonal_zero