English
The condition for an endomorphism f to be self-adjoint with respect to a pair of bilinear maps B and F is exactly the adjoint relation f ↔ f under (B, F).
Русский
Условие самосопряжённости конца f относительно пары билинейных отображений B и F — это ровно сопряжённость f по отношению к этим парам.
LaTeX
$$$\\text{IsPairSelfAdjoint } f\\;\\equiv\\; B\\,\\text{IsAdjointPair}\\, F\\; f\\; f$$$
Lean4
/-- The condition for an endomorphism to be "self-adjoint" with respect to a pair of bilinear maps
on the underlying module. In the case that these two maps are identical, this is the usual concept
of self adjointness. In the case that one of the maps is the negation of the other, this is the
usual concept of skew adjointness. -/
def IsPairSelfAdjoint (f : M → M) :=
IsAdjointPair B F f f
