toLinHomAux₁ — Mathlib

English

For a finite index set t, a family of vectors g(i) ∈ M, and w ∈ M, the bilinear form is additive in the left argument: B(∑_{i∈t} g(i), w) = ∑_{i∈t} B(g(i), w).

Русский

Для конечного множества индексов t и функций g: t → M, верно: B(∑_{i∈t} g(i), w) = ∑_{i∈t} B(g(i), w).

LaTeX

$$$$ B(\sum_{i\in t} g(i), w) = \sum_{i\in t} B(g(i), w). $$$$

Lean4

/-- Auxiliary definition to define `toLinHom`; see below. -/
def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R :=
  A x

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