Theorems · Theorem · linear algebra

LinearMap.sum_repr_mul_repr_mul

∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {Rₗ : Type u_10} {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13}
  [inst : CommSemiring Rₗ] [inst_1 : AddCommMonoid Mₗ] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ]
  [inst_4 : Module Rₗ Mₗ] [inst_5 : Module Rₗ Nₗ] [inst_6 : Module Rₗ Pₗ] (b₁' : Module.Basis ι₁ Rₗ Mₗ)
  (b₂' : Module.Basis ι₂ Rₗ Nₗ) {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x : Mₗ) (y : Nₗ),
  ((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y

Write out B x y as a sum over B (b i) (b j) if b is a basis. Version for bilinear maps, see sum_repr_mul_repr_mulₛₗ for the semi-bilinear version.

Defined in

Mathlib.LinearAlgebra.Basis.Bilinear

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModule