det_zero'' — Mathlib

English

Let M be a nontrivial finite free module over a commutative ring R. Then the determinant of the zero endomorphism on M is zero.

Русский

Пусть M является ненулевым конечномерным свободным модулем над коммутативной колецом R. Тогда детерминант нулевого отображения M → M равен нулю.

LaTeX

$$$$ \det(0: M \to M) = 0 $$$$

Lean4

@[simp high]
theorem det_zero'' {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
    [Nontrivial M] : LinearMap.det (0 : M →ₗ[R] M) = 0 :=
  by
  letI : Nonempty (Module.Free.ChooseBasisIndex R M) := (Module.Free.chooseBasis R M).index_nonempty
  nontriviality R
  exact LinearMap.det_zero' (Module.Free.chooseBasis R M)

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