isAdjointPair_symm_iff — Mathlib

English

For a bilinear form B and a linear equivalence f: M ≃ M, the pair (f, f^{-1}) is adjoint with respect to B if and only if f is orthogonal with respect to B.

Русский

Для билинейной формы B и линейного эквивалента f: M ≃ M пара (f, f^{-1}) является сопряжённой относительно B тогда и только тогда, когда f ортогонален относительно B.

LaTeX

$$$\\big(B\\IsAdjointPair B B f f^{-1}\\big) \\iff \\forall x,y,\\ B(f(x),f(y)) = B(x,y)$$$

Lean4

@[simp]
theorem _root_.LinearEquiv.isAdjointPair_symm_iff {f : M ≃ M} :
    LinearMap.IsAdjointPair B B f f.symm ↔ B.IsOrthogonal f :=
  ⟨fun hf x y ↦ by simpa using hf x (f y), fun hf x y ↦ by simpa using hf x (f.symm y)⟩

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