det_eq_zero_iff_ker_ne_bot — Mathlib

English

Over a domain with a finite free module, det f = 0 if and only if ker f is nontrivial.

Русский

В области с конечномерным свободным модулем det f = 0 тогда и только тогда, когда ker f не тривиально.

LaTeX

$$$\det f = 0 \iff \ker f \neq \{0\}$$$

Lean4

/-- The determinant of a map vanishes iff the map is not injective. -/
theorem det_eq_zero_iff_ker_ne_bot [IsDomain R] [Free R M] [Module.Finite R M] {f : M →ₗ[R] M} :
    f.det = 0 ↔ ker f ≠ ⊥ := by
  constructor <;> intro h
  · exact bot_lt_iff_ne_bot.mp (bot_lt_ker_of_det_eq_zero h)
  · let b := Module.finBasis R M
    obtain ⟨v, ⟨_, hv_ne_zero⟩⟩ := (ker f).ne_bot_iff.mp h
    rw [← det_toMatrix b, ← Matrix.exists_mulVec_eq_zero_iff]
    refine ⟨fun i => b.repr v i, by simpa, by simpa [toMatrix_mulVec_repr]⟩

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