Theorems · Definition · linear algebra

Matrix.frobeniusSeminormedAddCommGroup

{m : Type u_3} →
  {n : Type u_4} →
    {α : Type u_5} → [Fintype m] → [Fintype n] → [SeminormedAddCommGroup α] → SeminormedAddCommGroup (Matrix m n α)

Seminormed group instance (using the Frobenius norm) for matrices over a seminormed group. Not declared as an instance because there are several natural choices for defining the norm of a matrix.

Defined in

Mathlib.Analysis.Matrix.Normed

Cited by

18 results in Mathlib

Foundations

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

Assumes

FintypeFintypeSeminormedAddCommGroup