isOrtho_polarBilin — Mathlib

English

Orthogonality of a quadratic map equals orthogonality of its polar bilinear form.

Русский

Ортогональность квадратичной карты равна ортогональности её полярной билинейной формы.

LaTeX

$$$\\mathrm{IsOrtho}_{\\text{polarBilin}}(Q,x,y) \\iff \\mathrm{IsOrtho}(Q,x,y).$$$

Lean4

@[simp]
theorem isOrtho_polarBilin {x y : M} : Q.polarBilin.IsOrtho x y ↔ IsOrtho Q x y := by
  simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]

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