IsOrthogonal — Mathlib

English

A linear map f is orthogonal with respect to a bilinear form B if B(fx, fy) = B(x, y) for all x, y.

Русский

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

LaTeX

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

Lean4

/-- A linear transformation `f` is orthogonal with respect to a bilinear form `B` if `B` is
bi-invariant with respect to `f`. -/
def IsOrthogonal : Prop :=
  ∀ x y, B (f x) (f y) = B x y

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