Theorems · Definition · linear algebra

LinearMap.BilinForm.orthogonal

{R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.BilinForm R M → Submodule R M → Submodule R M

The orthogonal complement of a submodule N with respect to some bilinear form is the set of elements x which are orthogonal to all elements of N; i.e., for all y in N, B y x = 0. Note that for general (neither symmetric nor antisymmetric) bilinear forms this definition has a chirality; in addition to this "right" orthogonal complement one could define a "left" orthogonal complement for which, for all y in N, B x y = 0. This variant definition is not currently provided in mathlib.

Defined in

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

Cited by

36 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule