Theorems · Definition · linear algebra

Module.Basis.det

{R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {ι : Type u_4} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R M → M [⋀^ι]→ₗ[R] R

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

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

73 results in Mathlib

Foundations

Depth 93 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModuleDecidableEqFintype