Theorems · Theorem · linear algebra

LinearMap.toMatrix_prodMap

∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {M₁ : Type u_5} {M₂ : Type u_6} [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₁]
  [inst_6 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) [inst_7 : Fintype m]
  [inst_8 : DecidableEq m] [inst_9 : DecidableEq (n ⊕ m)] (φ₁ : Module.End R M₁) (φ₂ : Module.End R M₂),
  (LinearMap.toMatrix (v₁.prod v₂) (v₁.prod v₂)) (LinearMap.prodMap φ₁ φ₂) =
    Matrix.fromBlocks ((LinearMap.toMatrix v₁ v₁) φ₁) 0 0 ((LinearMap.toMatrix v₂ v₂) φ₂)

Defined in

Mathlib.LinearAlgebra.Matrix.ToLin

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringFintypeDecidableEqAddCommMonoidAddCommMonoidModuleModuleFintypeDecidableEqDecidableEq