det_zero' — Mathlib

English

If M has a finite basis and we consider the zero map, its determinant is zero.

Русский

Если M имеет конечный базис, то детерминант нулевого отображения равен нулю.

LaTeX

$$$\det(0) = 0$$$

Lean4

theorem det_zero' {ι : Type*} [Finite ι] [Nonempty ι] (b : Basis ι A M) : LinearMap.det (0 : M →ₗ[A] M) = 0 :=
  by
  haveI := Classical.decEq ι
  cases nonempty_fintype ι
  rwa [← det_toMatrix b, LinearEquiv.map_zero, det_zero]

Похожие утверждения