isSkewAdjoint_iff_neg_self_adjoint

English

An endomorphism f is skew-adjoint with respect to B if and only if the negation of B is an adjoint pair for f with respect to B.

Русский

Эндоморфизм f является косо-самосопряжённым по отношению к B тогда и только тогда, когда (−B) является сопряжённой парой для f относительно B.

LaTeX

$$B.IsSkewAdjoint f ↔ IsAdjointPair (−B) B f f$$

Lean4

theorem isSkewAdjoint_iff_neg_self_adjoint (f : M → M) : B.IsSkewAdjoint f ↔ IsAdjointPair (-B) B f f :=
  show (∀ x y, B (f x) y = B x ((-f) y)) ↔ ∀ x y, B (f x) y = (-B) x (f y) by simp

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