toLinearMapₛₗ₂'_apply — Mathlib

English

The pair (toMatrix₂Aux, toLinearMap₂'Aux) yields a bijection between bilinear maps and matrices.

Русский

Пара (toMatrix₂Aux, toLinearMap₂'Aux) образует биекцию между билинейными отображениями и матрицами.

LaTeX

$$$\text{toLinearMap₂'Aux}$ and $\text{toMatrix₂Aux}$ are inverse isomorphisms.$$

Lean4

theorem toLinearMapₛₗ₂'_apply (M : Matrix n m N₂) (x : n → R₁) (y : m → R₂) :
    -- porting note: we don't seem to have `∑ i j` as valid notation yet
    Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ M x y = ∑ i, ∑ j, σ₁ (x i) • σ₂ (y j) • M i j :=
  by
  rw [toLinearMapₛₗ₂', toMatrixₛₗ₂', LinearEquiv.coe_symm_mk, toLinearMap₂'Aux, mk₂'ₛₗ_apply]
  apply Finset.sum_congr rfl fun _ _ => Finset.sum_congr rfl fun _ _ => by rw [smul_comm]

Похожие утверждения