mathlib3 documentation


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 #

theorem linear_map.det_zero'' {R : Type u_1} {M : Type u_2} [comm_ring R] [add_comm_group M] [module R M] [ R M] [module.finite R M] [nontrivial M] :