toMatrix_mul — Mathlib

English

Similarly, multiplying BilinForm.toMatrix b B on the left by M corresponds to right-conjugating the bilinear form by the associated linear map.

Русский

Аналогично, умножение BilinForm.toMatrix b B слева матрицей M соответствует правой конъюгации билинейной формы соответствующим линейным отображением.

LaTeX

$$$$\mathrm{BilinForm.toMatrix}_{b}(B) \cdot M = \mathrm{BilinForm.toMatrix}_{b}\bigl(B \circ (\mathrm{Matrix.toLin}_{b b} M^{\top})\bigr).$$$$

Lean4

theorem toMatrix_mul (B : BilinForm R₁ M₁) (M : Matrix n n R₁) :
    BilinForm.toMatrix b B * M = BilinForm.toMatrix b (B.compRight (Matrix.toLin b b M)) :=
  LinearMap.toMatrix₂_mul _ _ _ B _

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