Theorems · Definition · linear algebra

Matrix.toLpLinAlgEquiv

{n : Type u_2} →
  {R : Type u_4} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] → (p : ENNReal) → Matrix n n R ≃ₐ[R] Module.End R (WithLp p (n → R))

Matrix.toLinAlgEquiv' adapted for PiLp R _.

Defined in

Mathlib.Analysis.Normed.Lp.Matrix

Cited by

4 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRing