Theorems · Definition · linear algebra

LinearMap.toMatrix

{R : Type u_1} →
  [inst : CommSemiring R] →
    {m : Type u_3} →
      {n : Type u_4} →
        [Fintype n] →
          [Finite m] →
            [DecidableEq n] →
              {M₁ : Type u_5} →
                {M₂ : Type u_6} →
                  [inst_4 : AddCommMonoid M₁] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          Module.Basis n R M₁ → Module.Basis m R M₂ → (M₁ →ₗ[R] M₂) ≃ₗ[R] Matrix m n R

Given bases of two modules M₁ and M₂ over a commutative ring R, we get a linear equivalence between linear maps M₁ →ₗ M₂ and matrices over R indexed by the bases.

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

180 results in Mathlib

Foundations

Depth 87 from the axioms, rests on 2,015 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringFintypeFiniteDecidableEqAddCommMonoidAddCommMonoidModuleModule