coe_dualBasis

Mathlib.LinearAlgebra.Dual.Basis

URI: https://scilib.ai/kg/mathlib#Module.DualBases.coe_dualBasis

English

The dual basis for h.basis coincides with ε; i.e., (h.basis.dualBasis)^coerced equals ε.

Русский

Двойственная база для h.basis равна ε.

LaTeX

$$$ \\text{coe}_\\text{dualBasis} : h.basis.dualBasis = ε $$$

Lean4

theorem coe_dualBasis [DecidableEq ι] [Finite ι] : ⇑h.basis.dualBasis = ε :=
  funext fun i => h.basis.ext fun j => by simp

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

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

Разделы

Аффилиация

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