Bilinear and quadratic forms

AbbreviationBilinear form#

For convenience, a shorthand for the type of bilinear forms from M to R.

LinearMap.BilinForm.{u_2, u_5} (R : Type u_2) [CommSemiring R] (M : Type u_5) [AddCommMonoid M]
  [_root_.Module R M] : Type (max u_2 u_5)

Sources

• Mathlib documentation: LinearMap.BilinForm
• Source of LinearMap.BilinForm in Mathlib/LinearAlgebra/BilinearMap.lean
• Mathlib overview: Linear algebra › Bilinear and quadratic forms
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Bilinear forms

MathlibLinearMap.BilinForm

Uses 1 · Used by 5

Statement usesLinear map

Used byAlternating bilinear form · Matrix representation · Symmetric bilinear form · Nondegenerate forms · Orthogonal elements

DefinitionAlternating bilinear form#

The proposition that a bilinear form is alternating

LinearMap.BilinForm.IsAlt.{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.IsAlt
• Source of LinearMap.BilinForm.IsAlt in Mathlib/LinearAlgebra/BilinearForm/Properties.lean
• Mathlib overview: Linear algebra › Bilinear and quadratic forms
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Bilinear forms

MathlibLinearMap.BilinForm.IsAlt

Uses 1

Statement usesBilinear form

StructureSymmetric bilinear form#

The proposition that a bilinear form is symmetric

LinearMap.BilinForm.IsSymm.{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.IsSymm
• Source of LinearMap.BilinForm.IsSymm in Mathlib/LinearAlgebra/BilinearForm/Properties.lean
• Mathlib overview: Linear algebra › Bilinear and quadratic forms
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Bilinear forms

MathlibLinearMap.BilinForm.IsSymm

Uses 1

Statement usesBilinear form

DefinitionMatrix representation#

BilinForm.toMatrix b is the equivalence between R-bilinear forms on M and n-by-n matrices with entries in R, if b is an R-basis for M.

LinearMap.BilinForm.toMatrix.{u_1, u_2, u_5} {R₁ : Type u_1} {M₁ : Type u_2} [CommSemiring R₁]
  [AddCommMonoid M₁] [_root_.Module R₁ M₁] {n : Type u_5} [Fintype n] [DecidableEq n]
  (b : Module.Basis n R₁ M₁) : LinearMap.BilinForm R₁ M₁ ≃ₗ[R₁] Matrix n n R₁

Sources

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

MathlibLinearMap.BilinForm.toMatrix

Uses 4 · Used by 1

Statement usesAssociative algebra over a commutative ring · Bilinear form · Isomorphism with \(K^n\) · Ring-valued matrix

Used byChange of coordinates

AbbreviationQuadratic form#

A quadratic form on a module.

QuadraticForm.{u, v} (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M]
  [_root_.Module R M] : Type (max u v)

Sources

• Mathlib documentation: QuadraticForm
• Source of QuadraticForm in Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
• Mathlib overview: Linear algebra › Bilinear and quadratic forms
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Quadratic forms

MathlibQuadraticForm

Uses 1 · Used by 4

Statement usesLinear map

Used byClifford algebra · Complex classification · Sylvester's law of inertia (existence) · Sylvester's law of inertia (uniqueness)

DefinitionPolar form of a quadratic#

Up to a factor 2, Q.polar is the associated bilinear map for a quadratic map Q.

Source of this name: https://en.wikipedia.org/wiki/Quadratic_form#Generalization

QuadraticMap.polar.{u_4, u_5} {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddCommGroup N]
  (f : M → N) (x y : M) : N

Sources

• Mathlib documentation: QuadraticMap.polar
• Source of QuadraticMap.polar in Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
• Mathlib overview: Linear algebra › Bilinear and quadratic forms
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Quadratic forms

MathlibQuadraticMap.polar

Uses 1 · Used by 1

Statement usesInteger

Used byComplex classification

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.