toMatrix₂Aux_apply — Mathlib

English

The two-way construction between bilinear maps and matrices is a genuine inverse; applying one after the other yields the original map.

Русский

Обратная конструкция между билинейными отображениями и матрицами восстанавливает исходное отображение после применения обеих операций.

LaTeX

$$$\text{(toMatrix₂Aux) and (toLinearMap₂'Aux) are mutual inverses}$$$

Lean4

@[simp]
theorem toMatrix₂Aux_apply (f : M₁ →ₛₗ[σ₁] M₂ →ₛₗ[σ₂] N₂) (b₁ : n → M₁) (b₂ : m → M₂) (i : n) (j : m) :
    LinearMap.toMatrix₂Aux R b₁ b₂ f i j = f (b₁ i) (b₂ j) :=
  rfl

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