Theorems · Theorem · linear algebra

basis_toMatrix_basisFun_mul

∀ {ι : Type u_1} {R : Type u_5} [inst : CommSemiring R] [inst_1 : Fintype ι] (b : Module.Basis ι R (ι → R))
  (A : Matrix ι ι R), b.toMatrix ⇑(Pi.basisFun R ι) * A = Matrix.of fun i j => (b.repr (A.col j)) i

Defined in

Mathlib.LinearAlgebra.Matrix.Basis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringFintype