mul_toMatrix₂ — Mathlib

English

A basis change inserted on both sides yields a direct equality between the transformed and original matrices B.

Русский

Замена базиса с обеих сторон приводит к равенству преобразованных и исходных матриц B.

LaTeX

$$$$ \bigl( b_1.toMatrix c_1 \bigr)^{\top} \; \mathrm{toMatrix}_2^{b_1,b_2} (B) \; \bigl( b_2.toMatrix c_2 \bigr) = \mathrm{toMatrix}_2^{c_1,c_2} (B). $$$$

Lean4

theorem mul_toMatrix₂ (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix n' n R) :
    M * LinearMap.toMatrix₂ b₁ b₂ B = LinearMap.toMatrix₂ b₁' b₂ (B.comp (toLin b₁' b₁ Mᵀ)) := by
  rw [LinearMap.toMatrix₂_comp b₁, toMatrix_toLin, transpose_transpose]

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