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

State before:
ι : Type ?u.134840
R : Type ?u.134843
l : Type ?u.134846
m : Type u_1
n : Type u_2
p : Type ?u.134855
q : Type ?u.134858
r : Type ?u.134861
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
A : Matrix m n ℝ
⊢ ‖A‖ = √(∑ i : m, ∑ j : n, ‖A i j‖ ^ 2)
Tactic:
rw [frobenius_norm_def, Real.sqrt_eq_rpow]
State after:
no goals