Theorems · Theorem · linear algebra

LinearMap.toMatrixAlgEquiv_mul

∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f g : M₁ →ₗ[R] M₁),
  (LinearMap.toMatrixAlgEquiv v₁) (f * g) = (LinearMap.toMatrixAlgEquiv v₁) f * (LinearMap.toMatrixAlgEquiv v₁) g

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites14

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

DFunLike.coestatement and proof · cited by 62,936
Modulestatement and proof · cited by 20,661
RingHom.idstatement and proof · cited by 18,349
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
LinearMapstatement and proof · cited by 10,215
Fintypestatement and proof · cited by 7,736
Matrixstatement and proof · cited by 4,303
AlgEquivstatement · cited by 1,681
Module.Basisstatement and proof · cited by 1,477
Module.Endproof · cited by 774
LinearMap.toMatrixAlgEquivstatement and proof · cited by 19

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.