English
Under a finite basis, the zero endomorphism has determinant zero; under a generalization, det_zero' holds with an explicit basis choice.
Русский
При наличии конечного базиса нулевой эндоморфизм имеет det = 0; в общем виде формулировка det_zero' включает явный выбор базиса.
LaTeX
$$$\det(0) = 0$$$
Lean4
/-- In a finite-dimensional vector space, the zero map has determinant `1` in dimension `0`,
and `0` otherwise. We give a formula that also works in infinite dimension, where we define
the determinant to be `1`. -/
@[simp]
theorem det_zero [Module.Free A M] : LinearMap.det (0 : M →ₗ[A] M) = (0 : A) ^ Module.finrank A M := by
simp only [← zero_smul A (1 : M →ₗ[A] M), det_smul, mul_one, MonoidHom.map_one]
