English
A product identity expresses the relation between a left multiplier M, a bilinear map B, and a right multiplier N via a composed compl₁₂ object.
Русский
Существуют соотношения между левым множителем M, билинейным отображением B и правым множителем N через составленный объект compl₁₂.
LaTeX
$$$$ M \cdot \mathrm{toMatrix}_2^{b_1,b_2} (B) \cdot N = \mathrm{toMatrix}_2^{b_1',b_2'} \Bigl( B \!\!\mathrm{compl}_{12} \bigl( \mathrm{toLin}_{b_1',b_1} M^{\!T} \bigr) \!\! \bigl( \mathrm{toLin}_{b_2',b_2} N \bigr) \Bigr). $$$$
Lean4
@[simp]
theorem toMatrix₂_mul_basis_toMatrix (c₁ : Basis n' R M₁) (c₂ : Basis m' R M₂) (B : M₁ →ₗ[R] M₂ →ₗ[R] R) :
(b₁.toMatrix c₁)ᵀ * LinearMap.toMatrix₂ b₁ b₂ B * b₂.toMatrix c₂ = LinearMap.toMatrix₂ c₁ c₂ B :=
by
simp_rw [← LinearMap.toMatrix_id_eq_basis_toMatrix]
rw [← LinearMap.toMatrix₂_compl₁₂, LinearMap.compl₁₂_id_id]
