Multilinearity

• Multilinear map

DefinitionDeterminant of vectors#

The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.

Module.Basis.det.{u_1, u_2, u_4} {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M]
  [_root_.Module R M] {ι : Type u_4} [DecidableEq ι] [Fintype ι] (e : Module.Basis ι R M) :
  M [⋀^ι]→ₗ[R] R

Sources

• Mathlib documentation: Module.Basis.det
• Source of Module.Basis.det in Mathlib/LinearAlgebra/Determinant.lean
• Mathlib undergraduate list: Linear algebra › Multilinearity

MathlibModule.Basis.det

Uses 2 · Used by 1

Statement usesBasis · Determinant

Used byInscribed angle theorem

DefinitionDeterminant of endomorphisms#

The determinant of an endomorphism independent of basis.

If there is no finite basis on M, the result is 1 instead.

LinearMap.det.{u_2, u_5} {M : Type u_2} [AddCommGroup M] {A : Type u_5} [CommRing A]
  [_root_.Module A M] : (M →ₗ[A] M) →* A

Sources

• Mathlib documentation: LinearMap.det
• Source of LinearMap.det in Mathlib/LinearAlgebra/Determinant.lean
• Mathlib undergraduate list: Linear algebra › Multilinearity

MathlibLinearMap.det

Uses 3 · Used by 1

Statement usesAlgebra of endomorphisms of a vector space · Determinant · Matrix representation of a linear map

Used byChange of variables formula

DefinitionSpecial linear group#

SpecialLinearGroup n R is the group of n by n R-matrices with determinant equal to 1.

Matrix.SpecialLinearGroup.{u, v} (n : Type u) [DecidableEq n] [Fintype n] (R : Type v)
  [CommRing R] : Type (max 0 u v)

Sources

• Mathlib documentation: Matrix.SpecialLinearGroup
• Source of Matrix.SpecialLinearGroup in Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
• Mathlib undergraduate list: Linear algebra › Multilinearity
• Mathlib undergraduate list: Group Theory › Classical automorphism groups

MathlibMatrix.SpecialLinearGroup

Uses 1

Statement usesDeterminant

AbbreviationOrientation of a \(\R\)-vector space#

An orientation of a module, intended to be used when ι is a Fintype with the same cardinality as a basis.

Orientation.{u_1, u_2, u_4} (R : Type u_1) [CommSemiring R] [PartialOrder R] [IsStrictOrderedRing R]
  (M : Type u_2) [AddCommMonoid M] [_root_.Module R M] (ι : Type u_4) : Type (max (max u_4 u_1) u_2)

Sources

• Mathlib documentation: Orientation
• Source of Orientation in Mathlib/LinearAlgebra/Orientation.lean
• Mathlib undergraduate list: Linear algebra › Multilinearity

MathlibOrientation

Uses 2 · Used by 1

Statement usesAlternating map · Associative algebra over a commutative ring

Used byInscribed angle theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.