IsSelfAdjoint — Mathlib

English

An endomorphism f is self-adjoint with respect to a bilinear form B if B(fx, y) = B(x, fy) for all x,y.

Русский

Конец f самосопряжён относительно билинейной формы B, если выполняется B(fx, y) = B(x, fy) для всех x,y.

LaTeX

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

Lean4

/-- An endomorphism of a module is self-adjoint with respect to a bilinear map if it serves as an
adjoint for itself. -/
protected def IsSelfAdjoint (f : M → M) :=
  IsAdjointPair B B f f

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