English
Let B be a bilinear form on a finite module M, and let b and c be two bases of M. Then the matrix of B in basis c is obtained from the matrix of B in basis b by the congruence with the change-of-basis matrix from c to b, i.e. BilinForm.toMatrix c B = (b.toMatrix c)^T · BilinForm.toMatrix b B · b.toMatrix c.
Русский
Пусть B — билинейная форма на конечном модуле M, и пусть b и c — две базы M. Тогда матрица B в базе c равна конгруэнтному преобразованию матрицы B в базе b с переходной матрицей из c в b: BilinForm.toMatrix c B = (b.toMatrix c)^T · BilinForm.toMatrix b B · b.toMatrix c.
LaTeX
$$$$\text{BilinForm.toMatrix}_{c}(B) = (\text{b.toMatrix}_{c})^{T} \; \text{BilinForm.toMatrix}_{b}(B) \; (\text{b.toMatrix}_{c}).$$$$
Lean4
@[simp]
theorem toMatrix_mul_basis_toMatrix (c : Basis o R₁ M₁) (B : BilinForm R₁ M₁) :
(b.toMatrix c)ᵀ * BilinForm.toMatrix b B * b.toMatrix c = BilinForm.toMatrix c B :=
LinearMap.toMatrix₂_mul_basis_toMatrix _ _ _ _ B
