toDualFlip — Mathlib

English

The map toDualFlip is the transpose-like operation of toDual, defined by b.toDualFlip(m) = b.toDual(·) with the arguments swapped, i.e., toDualFlip m1 m2 = toDual m2 m1.

Русский

Операция toDualFlip есть преобразование, в котором аргументы разворачиваются: toDualFlip m1 m2 = toDual m2 m1.

LaTeX

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

Lean4

/-- `h.toDualFlip v` is the linear map sending `w` to `h.toDual w v`. -/
def toDualFlip (m : M) : M →ₗ[R] R :=
  b.toDual.flip m

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