Proposition 3
Tag 0646, permanent. Cite it as [Bourbaki, Tag 0646].
Algebra, chapter III, § 8. Determinants
Let be a finite-dimensional free -module. For every endomorphism of , the following conditions are equivalent: (f) is injective; (g) det is not a divisor of zero in .
With the same notation as in the proof of Theorem 1, for to be injective, it is necessary and sufficient that the be linearly independent. By § 7, no. 9, Proposition 12, it is necessary and sufficient for this that the relation (with ) imply . But this is equivalent to since is a basis of ; whence the proposition.
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.