Theorems · Theorem · linear algebra

Matrix.linfty_opNNNorm_mul

∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : NonUnitalSeminormedRing α] (A : Matrix l m α) (B : Matrix m n α),
  ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊

Defined in

Mathlib.Analysis.Matrix.Normed

Cited by

2 results in Mathlib

Foundations

Depth 232 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeFintypeFintypeNonUnitalSeminormedRing