toDualEquiv_apply

Mathlib.LinearAlgebra.Dual.Basis

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

English

For any m ∈ M, the image under the dual equivalence equals the toDual image: toDualEquiv(m) = toDual(m).

Русский

Для любого m ∈ M образ через дуальную эквивалентность равен образу через toDual: toDualEquiv(m) = toDual(m).

LaTeX

$$$ toDualEquiv(m) = toDual(m). $$$

Lean4

@[simp]
theorem toDualEquiv_apply (m : M) : b.toDualEquiv m = b.toDual m :=
  rfl

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

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

Разделы

Аффилиация

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