Theorems · Theorem · linear algebra

LinearMap.toMatrix_id_eq_basis_toMatrix

∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (b' : Module.Basis ι' R M) [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] [inst_5 : Finite ι'], (LinearMap.toMatrix b b') LinearMap.id = b'.toMatrix ⇑b

A generalization of LinearMap.toMatrix_id.

Defined in

Mathlib.LinearAlgebra.Matrix.Basis

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFintypeDecidableEqFinite