case pos
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)

case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
by_cases hf : Summable f
no goals
case pos
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
exact hf.hasSum.matrix_diagonal.tsum_eq.symm
case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
have hft := summable_matrix_diagonal.not.mpr hf
case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal 0 = 0
case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal (∑' (x : X), f x) = ∑' (x : X), diagonal (f x)
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft]
no goals
case neg
X : Type u_3
α : Type ?u.78999
l : Type ?u.79002
m : Type ?u.79005
n : Type u_1
p : Type ?u.79011
S : Type ?u.79014
R : Type u_2
m' : l → Type ?u.79022
n' : l → Type ?u.79027
inst✝⁵ : Semiring α
inst✝⁴ : AddCommMonoid R
inst✝³ : TopologicalSpace R
inst✝² : Module α R
inst✝¹ : DecidableEq n
inst✝ : T2Space R
f : X → n → R
hf : ¬Summable f
hft : ¬Summable fun x => diagonal (f x)
⊢ diagonal 0 = 0
exact diagonal_zero