repr_symm_single_one

Mathlib.LinearAlgebra.Basis.Defs

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

English

For any i, the preimage of the unit δ_i under repr^{-1} equals the i-th basis vector.

Русский

Для любого i предобраз δ_i под repr^{-1} равен i-му вектору базиса.

LaTeX

$$$b.\mathrm{repr}^{-1}(\delta_i) = b_i$$$

Lean4

theorem repr_symm_single_one : b.repr.symm (Finsupp.single i 1) = b i :=
  rfl

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

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

Разделы

Аффилиация

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