Theorems · Theorem · linear algebra

Matrix.liftLinear_comp_singleLinearMap

∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : AddCommMonoid β] [inst_8 : Module R α] [inst_9 : Module R β]
  [inst_10 : Module S β] [inst_11 : SMulCommClass R S β] (f : m → n → α →ₗ[R] β) (i : m) (j : n),
  (Matrix.liftLinear S) f ∘ₗ Matrix.singleLinearMap R i j = f i j

Defined in

Mathlib.Data.Matrix.Basis

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqFintypeFintypeSemiringSemiringAddCommMonoidAddCommMonoidModuleModuleModuleSMulCommClass