Theorems · Definition · linear algebra

algEquivMatrix

{R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_3} →
      [inst_1 : DecidableEq n] →
        {M : Type u_4} →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] → [inst_4 : Fintype n] → Module.Basis n R M → Module.End R M ≃ₐ[R] Matrix n n R

A basis of a module induces an equivalence of algebras from the endomorphisms of the module to square matrices.

Defined in: Mathlib.LinearAlgebra.Matrix.ToLin
Cited by: 1 results in Mathlib
Foundations: Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring DecidableEq AddCommMonoid Module Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Fintypestatement and proof · cited by 7,736
Matrixstatement · cited by 4,303
AlgEquivstatement · cited by 1,681
Module.Basisstatement and proof · cited by 1,477
Module.Endstatement · cited by 774
AlgEquiv.transproof · cited by 108
Module.Basis.equivFunproof · cited by 88
LinearEquiv.conjAlgEquivproof · cited by 15
algEquivMatrix'proof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

LinearMap.aeval_self_charpolyproof · cited by 6