Theorems · Definition · linear algebra

Algebra.leftMulMatrix

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          {m : Type u_3} → [inst_3 : Fintype m] → [inst_4 : DecidableEq m] → Module.Basis m R S → S →ₐ[R] Matrix m m R

leftMulMatrix b x is the matrix corresponding to the linear map fun y ↦ x * y. leftMulMatrix_eq_repr_mul gives a formula for the entries of leftMulMatrix. This definition is useful for doing (more) explicit computations with LinearMap.mulLeft, such as the trace form or norm map for algebras.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

37 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraFintypeDecidableEq