toMatrix₂Aux_eq — Mathlib

English

A bilinear map's matrix under compl₂ with left/right maps equals the product of the matrices representing the left and right maps with the bilinear map matrix in between.

Русский

Матрица билинейного отображения после compl₂ слева/справа равна произведению матриц левых и правых отображений и матрицы самого отображения.

LaTeX

$$$\mathrm{toMatrix}_{2}' R (B.\!\mathrm{compl}_{2} f) = \mathrm{toMatrix}_{2}' R B \star \mathrm{toMatrix}' f.$$$

Lean4

theorem toMatrix₂Aux_eq (B : M₁ →ₗ[R] M₂ →ₗ[R] N₂) : LinearMap.toMatrix₂Aux R b₁ b₂ B = LinearMap.toMatrix₂ b₁ b₂ B :=
  Matrix.ext fun i j => by rw [LinearMap.toMatrix₂_apply, LinearMap.toMatrix₂Aux_apply]

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