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] :