case pos
X : Type u_4
α : Type ?u.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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_conjTranspose.tsum_eq.symm
case neg
X : Type u_4
α : Type ?u.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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_conjTranspose.not.mpr hf
no goals
case neg
X : Type u_4
α : Type ?u.67432
l : Type ?u.67435
m : Type u_2
n : Type u_3
p : Type ?u.67444
S : Type ?u.67447
R : Type u_1
m' : l → Type ?u.67455
n' : l → Type ?u.67460
inst✝⁶ : Semiring α
inst✝⁵ : AddCommMonoid R
inst✝⁴ : TopologicalSpace R
inst✝³ : Module α R
inst✝² : StarAddMonoid R
inst✝¹ : ContinuousStar 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, conjTranspose_zero]