toDual_apply_left — Mathlib

English

For any m ∈ M and i ∈ ι, the dual pairing with basis vector b_i yields the i-th coordinate of m in the basis b, i.e., b.toDual(m)(b_i) = b.repr(m,i).

Русский

Для любого m ∈ M и i ∈ ι скалярное отображение дуального пространства на базисный вектор b_i дает i-ю координату представления m в базисе b: b.toDual(m)(b_i) = b.repr(m,i).

LaTeX

$$$ b.toDual m (b i) = b.repr m i. $$$

Lean4

theorem toDual_apply_left (m : M) (i : ι) : b.toDual m (b i) = b.repr m i := by
  rw [← b.toDual_linearCombination_left, b.linearCombination_repr]

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