toDual_apply_right

Mathlib.LinearAlgebra.Dual.Basis

URI: https://scilib.ai/kg/mathlib#Module.Basis.toDual_apply_right

English

Similarly, the i-th coordinate of m with respect to b is given by b.toDual(b_i)(m) = b.repr(m,i).

Русский

Аналогично, i-я координата m относительно базиса b равна b.toDual(b_i)(m) = b.repr(m,i).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru