feat(analysis/normed_space/basic): norm_entry_le_entrywise_sup_norm (…

…#12159)

The entries of a matrix are at most the entrywise sup norm.


Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>

src/analysis/normed_space/basic.lean

@@ -791,6 +791,11 @@ def matrix.normed_space {α : Type*} [normed_field α] {n m : Type*} [fintype n]
   normed_space α (matrix n m α) :=
 pi.normed_space
 
+lemma matrix.norm_entry_le_entrywise_sup_norm {α : Type*} [normed_field α] {n m : Type*} [fintype n]
+  [fintype m] (M : (matrix n m α)) {i : n} {j : m} :
+  ∥M i j∥ ≤ ∥M∥ :=
+(norm_le_pi_norm (M i) j).trans (norm_le_pi_norm M i)
+
 end
 
 end normed_group