Theorems · Definition · linear algebra

Matrix.toLin

{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₂ → Matrix m n R ≃ₗ[R] M₁ →ₗ[R] M₂

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

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

77 results in Mathlib

Foundations

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

Assumes

CommSemiringFintypeFiniteDecidableEqAddCommMonoidAddCommMonoidModuleModule