Theorem: MatrixCookbook.eq_525 (MatrixCookbook/10FunctionsAndOperators.lean)

State before:
ι : Type ?u.77109
R : Type ?u.77112
l : Type ?u.77115
m : Type ?u.77118
n : Type u_1
p : Type ?u.77124
q : Type ?u.77127
r : Type ?u.77130
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
x : n → ℂ
⊢ ‖(WithLp.equiv 1 (n → ℂ)).symm x‖ = ∑ i : n, Complex.abs (x i)
Tactic:
simpa using PiLp.norm_eq_of_nat 1 Nat.cast_one.symm ((WithLp.equiv 1 _).symm x)
State after:
no goals