IsSkewAdjoint — Mathlib

English

An endomorphism f is skew-adjoint with respect to B if B(fx, y) = - B(x, f y) for all x, y; equivalently, f is adjoint to itself with respect to the pair (-B, B).

Русский

Эндоморфизм f скользяще‑сам сопряжён относительно B, если для всех x,y выполняется B(fx, y) = - B(x, f y); эквивалентно, f является сопряжённым к самому себе по паре (-B, B).

LaTeX

$$$\\forall x,y,\\ B(f(x), y) = - B(x, f(y))$$$

Lean4

/-- An endomorphism of a module is skew-adjoint with respect to a bilinear map if its negation
serves as an adjoint. -/
def IsSkewAdjoint (f : M → M) :=
  IsAdjointPair B B f (-f)

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