English
If B is symmetric, then the right dual basis property holds: B(b_i, dualBasis_j) = δ_{ij}. This follows from the left version by symmetry.
Русский
Если B симметрична, то правая база двойственной базы удовлетворяет B(b_i, dualBasis_j) = δ_{ij}. Это следует из левой версии благодаря симметрии.
LaTeX
$$$B\\big(b_i, B.dualBasis hB b j\\big) = \\delta_{ij}.$$$
Lean4
/-- The tensor product of two bilinear maps injects into bilinear maps on tensor products.
Note this is heterobasic; the bilinear map on the left can take values in a module over a
(commutative) algebra over the ring of the module in which the right bilinear map is valued. -/
def tensorDistrib : (BilinMap A M₁ N₁ ⊗[R] BilinMap R M₂ N₂) →ₗ[A] BilinMap A (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂) :=
(TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) (N₁ ⊗[R] N₂)).symm.toLinearMap ∘ₗ
((LinearMap.llcomp A _ _ _).flip
(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R A A M₁ M₂ M₁ M₂).toLinearMap) ∘ₗ
TensorProduct.AlgebraTensorModule.homTensorHomMap R _ _ _ _ _ _ ∘ₗ
(TensorProduct.AlgebraTensorModule.congr (TensorProduct.lift.equiv A M₁ M₁ N₁)
(TensorProduct.lift.equiv R _ _ _)).toLinearMap
