Theorems · Theorem · functional analysis

PiLp.basis_toMatrix_basisFun_mul

∀ (p : ENNReal) {ι : Type u_2} [inst : Fintype ι] {𝕜 : Type u_5} [inst_1 : SeminormedCommRing 𝕜]
  (b : Module.Basis ι 𝕜 (PiLp p fun x => 𝕜)) (A : Matrix ι ι 𝕜),
  b.toMatrix ⇑(PiLp.basisFun p 𝕜 ι) * A = Matrix.of fun i j => (b.repr (WithLp.toLp p (A.transpose j))) i

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeSeminormedCommRing