Determinants in free (finite) modules #
Quite a lot of our results on determinants (that you might know in vector spaces) will work for all free (finite) modules over any commutative ring.
Main results #
LinearMap.det_zero'': The determinant of the constant zero map is zero, in a finite free nontrivial module.
@[simp]
theorem
LinearMap.det_zero''
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
[Module.Free R M]
[Module.Finite R M]
[Nontrivial M]
:
LinearMap.det 0 = 0