Theorems · Theorem · linear algebra

Matrix.frobenius_nnnorm_def

∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α), ‖A‖₊ = (∑ i, ∑ j, ‖A i j‖₊ ^ 2) ^ (1 / 2)

Defined in

Mathlib.Analysis.Matrix.Normed

Cited by

5 results in Mathlib

Foundations

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

Assumes

FintypeFintypeSeminormedAddCommGroup