toDualFlip_apply

Mathlib.LinearAlgebra.Dual.Basis

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

English

The equality in toDualFlip is direct, namely for all m1, m2 in M, toDualFlip m1 m2 = toDual m2 m1.

Русский

Неравенство в toDualFlip тривиально: для любых m1, m2 ∈ M выполняется toDualFlip m1 m2 = toDual m2 m1.

LaTeX

$$$ b.toDualFlip (m_1) (m_2) = b.toDual (m_2) (m_1). $$$

Lean4

theorem toDualFlip_apply (m₁ m₂ : M) : b.toDualFlip m₁ m₂ = b.toDual m₂ m₁ :=
  rfl

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

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

Разделы

Аффилиация

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