case pos
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ

case neg
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
by_cases hf : Summable f
no goals
case pos
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
exact hf.hasSum.matrix_transpose.tsum_eq.symm
case neg
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᵀ
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
case neg
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
have hft := summable_matrix_transpose.not.mpr hf
no goals
case neg
X : Type u_4
α : Type ?u.51831
l : Type ?u.51834
m : Type u_2
n : Type u_3
p : Type ?u.51843
S : Type ?u.51846
R : Type u_1
m' : l → Type ?u.51854
n' : l → Type ?u.51859
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid R
inst✝² : TopologicalSpace R
inst✝¹ : Module α R
inst✝ : T2Space R
f : X → Matrix m n R
hf : ¬Summable f
hft : ¬Summable fun x => (f x)ᵀ
⊢ (∑' (x : X), f x)ᵀ = ∑' (x : X), (f x)ᵀ
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hft, transpose_zero]