Theorems · Definition · linear algebra

Matrix.toLpLin

{m : Type u_1} →
  {n : Type u_2} →
    {R : Type u_4} →
      [Fintype n] →
        [DecidableEq n] →
          [inst : CommRing R] → (p q : ENNReal) → Matrix m n R ≃ₗ[R] WithLp p (n → R) →ₗ[R] WithLp q (m → R)

Matrix.toLin' adapted for PiLp R _.

Defined in

Mathlib.Analysis.Normed.Lp.Matrix

Cited by

14 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommRing