Bilinear forms

• Bilinear forms
• Alternating bilinear forms
• Symmetric bilinear forms

AbbreviationNondegenerate forms#

A nondegenerate bilinear form is a bilinear form that is both left-separating and right-separating, i.e. if B x y = 0 for all y then x = 0, and if B x y = 0 for all x then y = 0.

Note that these conditions are independent of each other in general, but in the common case of finite-dimensional vector spaces (or, more generally, finite free modules over an integral domain), either of these conditions implies the other; see LinearMap.BilinForm.Nondegenerate.ofSeparatingLeft and LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot, proved in a later file.

LinearMap.BilinForm.Nondegenerate.{u_1, u_2} {R : Type u_1} {M : Type u_2} [CommSemiring R]
  [AddCommMonoid M] [_root_.Module R M] (B : LinearMap.BilinForm R M) : Prop

Sources

• Mathlib documentation: LinearMap.BilinForm.Nondegenerate
• Source of LinearMap.BilinForm.Nondegenerate in Mathlib/LinearAlgebra/BilinearForm/Properties.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Bilinear forms

MathlibLinearMap.BilinForm.Nondegenerate

Uses 1 · Used by 1

Statement usesBilinear form

Used byAdjoint endomorphism

• Matrix representation

TheoremChange of coordinates#

Mathlib states this as LinearMap.BilinForm.toMatrix_comp.

LinearMap.BilinForm.toMatrix_comp.{u_1, u_2, u_5, u_6, u_7} {R₁ : Type u_1} {M₁ : Type u_2}
  [CommSemiring R₁] [AddCommMonoid M₁] [_root_.Module R₁ M₁] {n : Type u_5} {o : Type u_6}
  [Fintype n] [Fintype o] [DecidableEq n] (b : Module.Basis n R₁ M₁) {M₂' : Type u_7}
  [AddCommMonoid M₂'] [_root_.Module R₁ M₂'] (c : Module.Basis o R₁ M₂') [DecidableEq o]
  (B : LinearMap.BilinForm R₁ M₁) (l r : M₂' →ₗ[R₁] M₁) :
  (LinearMap.BilinForm.toMatrix c) (B.comp l r) =
    ((LinearMap.toMatrix c b) l).transpose * (LinearMap.BilinForm.toMatrix b) B *
      (LinearMap.toMatrix c b) r

Sources

• Mathlib documentation: LinearMap.BilinForm.toMatrix_comp
• Source of LinearMap.BilinForm.toMatrix_comp in Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Bilinear forms

MathlibLinearMap.BilinForm.toMatrix_comp

Uses 2

Statement usesMatrix representation · Matrix representation of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.