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 nontrivial module.
@[simp]
theorem
linear_map.det_zero''
{R : Type u_1}
{M : Type u_2}
[comm_ring R]
[add_comm_group M]
[module R M]
[module.free R M]
[module.finite R M]
[nontrivial M] :
⇑linear_map.det 0 = 0