Determinants in free (finite) modules #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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 #
linear_map.det_zero'': The determinant of the constant zero map is zero, in a finite free