English
The determinant of a linear map represented by a matrix equals the determinant of the matrix itself.
Русский
Детерминант линейного отображения, задаваемого матрицей, равен детерминанту самой матрицы.
LaTeX
$$$\det(\mathrm{toLin}\, b\, b\, f) = \det f$$$
Lean4
/-- Multiplying a map by a scalar `c` multiplies its determinant by `c ^ dim M`. -/
@[simp]
theorem det_smul [Module.Free A M] (c : A) (f : M →ₗ[A] M) :
LinearMap.det (c • f) = c ^ Module.finrank A M * LinearMap.det f :=
by
nontriviality A
by_cases H : ∃ s : Finset M, Nonempty (Basis s A M)
· have : Module.Finite A M := by
rcases H with ⟨s, ⟨hs⟩⟩
exact Module.Finite.of_basis hs
simp only [← det_toMatrix (Module.finBasis A M), LinearEquiv.map_smul, Fintype.card_fin, Matrix.det_smul]
·
classical
have : Module.finrank A M = 0 := finrank_eq_zero_of_not_exists_basis H
simp [coe_det, H, this]
