Theorems · Theorem · linear algebra

Matrix.liftLinear_apply

∀ {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] β) (M : Matrix m n α),
  ((Matrix.liftLinear S) f) M = ∑ i, ∑ j, (f i j) (M i j)

Defined in

Mathlib.Data.Matrix.Basis

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqFintypeFintypeSemiringSemiringAddCommMonoidAddCommMonoidModuleModuleModuleSMulCommClass