English
If det f = 0, then the kernel of f is nontrivial (not equal to {0}).
Русский
Если det f = 0, то ядро f не тривиально.
LaTeX
$$$\det f = 0 \Rightarrow \ker f \neq \{0\}$$$
Lean4
/-- If the determinant of a map vanishes, then the map is not injective. -/
theorem bot_lt_ker_of_det_eq_zero [IsDomain R] [Free R M] {f : M →ₗ[R] M} (hf : f.det = 0) : ⊥ < ker f :=
by
have : Module.Finite R M := by simp [finite_of_det_ne_one (f := f), hf]
let b := Module.finBasis R M
suffices ∃ x, f x = 0 ∧ x ≠ 0 by simpa [bot_lt_iff_ne_bot, ker_eq_bot']
obtain ⟨v, hv_ne_zero, hv_zero⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr (det_toMatrix b f ▸ hf)
refine ⟨b.equivFun.symm v, ?_, b.equivFun.symm.map_ne_zero_iff.mpr hv_ne_zero⟩
rw [← b.equivFun.injective.eq_iff]
simp_all [funext_iff, Matrix.mulVec, dotProduct, toMatrix_apply, mul_comm]
