Theorems · Definition · linear algebra

LinearMap.detAux

{M : Type u_7} →
  [inst : AddCommGroup M] →
    {ι : Type u_8} →
      [DecidableEq ι] →
        [Fintype ι] →
          {A : Type u_9} → [inst_3 : CommRing A] → [inst_4 : Module A M] → Trunc (Module.Basis ι A M) → (M →ₗ[A] M) →* A

The determinant of an endomorphism given a basis. See LinearMap.det for a version that populates the basis non-computably. Although the Trunc (Basis ι A M) parameter makes it slightly more convenient to switch bases, there is no good way to generalize over universe parameters, so we can't fully state in detAux's type that it does not depend on the choice of basis. Instead you can use the detAux_def'' lemma, or avoid mentioning a basis at all using LinearMap.det.

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

10 results in Mathlib

Foundations

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

Assumes

AddCommGroupDecidableEqFintypeCommRingModule