English
Determinant of a matrix-to-linear-map construction equals the determinant of the matrix.
Русский
Детерминант преобразования матрица→линейное отображение равен детерминанту самой матрицы.
LaTeX
$$$\det(\mathrm{toLin}'\, f) = \det f$$$
Lean4
/-- To show `P (LinearMap.det f)` it suffices to consider `P (Matrix.det (toMatrix _ _ f))` and
`P 1`. -/
@[elab_as_elim]
theorem det_cases [DecidableEq M] {P : A → Prop} (f : M →ₗ[A] M)
(hb : ∀ (s : Finset M) (b : Basis s A M), P (Matrix.det (toMatrix b b f))) (h1 : P 1) : P (LinearMap.det f) := by
classical
if H : ∃ s : Finset M, Nonempty (Basis s A M) then
obtain ⟨s, ⟨b⟩⟩ := H
rw [← det_toMatrix b]
exact hb s b
else rwa [LinearMap.det_def, dif_neg H]
