toMatrix₂_mul — Mathlib

English

A simp-lemma expresses the same relation as above in a streamlined form for basis toMatrix.

Русский

Упрощающее утверждение отражает ту же связь в упрощённой форме для преобразования через базис.

LaTeX

$$$$ \text{(simplified)} \; (b_1.toMatrix c_1)^T \mathrm{toMatrix}_2^{b_1,b_2}(B) \; b_2.toMatrix c_2 = \mathrm{toMatrix}_2^{c_1,c_2}(B). $$$$

Lean4

theorem toMatrix₂_mul (B : M₁ →ₗ[R] M₂ →ₗ[R] R) (M : Matrix m m' R) :
    LinearMap.toMatrix₂ b₁ b₂ B * M = LinearMap.toMatrix₂ b₁ b₂' (B.compl₂ (toLin b₂' b₂ M)) := by
  rw [LinearMap.toMatrix₂_compl₂ b₁ b₂, toMatrix_toLin]

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