rw [norm_smul r A, Real.norm_eq_abs]
ι : Type ?u.93818
R : Type ?u.93821
l : Type ?u.93824
m : Type ?u.93827
n : Type u_1
p : Type ?u.93833
q : Type ?u.93836
r✝ : Type ?u.93839
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
r : ℝ
A : Matrix n n ℝ
⊢ ‖r • A‖ = |r| * ‖A‖
no goals