dotProductBilin — Mathlib

English

The dot product is bilinear in its two vector arguments.

Русский

Скалярное произведение билинейно по обоим векторам.

LaTeX

$$dotProductBilin : (m → A) →ₗ[R] (m → A) →ₗ[S] A$$

Lean4

/-- `vecMulVec` as a bilinear map.

When `A` is noncommutative, `R` and `S` can be instantiated as `vecMulVecLinear A Aᵐᵒᵖ`. -/
@[simps]
def dotProductBilin [Fintype m] : (m → A) →ₗ[R] (m → A) →ₗ[S] A
    where
  toFun
    x :=
    { toFun y := dotProduct x y
      map_add' _ _ := dotProduct_add _ _ _
      map_smul' _ _ := dotProduct_smul _ _ _ }
  map_add' _ _ := LinearMap.ext fun _ => add_dotProduct _ _ _
  map_smul' _ _ := LinearMap.ext fun _ => smul_dotProduct _ _ _

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