Theorems · Theorem · linear algebra

LinearMap.det_zero

∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] [Module.Free A M],
  LinearMap.det 0 = 0 ^ Module.finrank A M

In a finite-dimensional vector space, the zero map has determinant 1 in dimension 0, and 0 otherwise. We give a formula that also works in infinite dimension, where we define the determinant to be 1.

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommGroupCommRingModuleModule.Free