det_coe_symm — Mathlib

English

The determinant of the inverse of a linear equivalence equals the inverse of the determinant.

Русский

Детерминант обратного линейного эквивалента равен обратному детерминанту исходного.

LaTeX

$$$\det(f^{-1}) = (\det f)^{-1}$$$

Lean4

/-- The determinant of `f.symm` is the inverse of that of `f` when `f` is a linear equiv. -/
theorem det_coe_symm {𝕜 : Type*} [Field 𝕜] [Module 𝕜 M] (f : M ≃ₗ[𝕜] M) :
    LinearMap.det (f.symm : M →ₗ[𝕜] M) = (LinearMap.det (f : M →ₗ[𝕜] M))⁻¹ := by
  simp [field, IsUnit.ne_zero f.isUnit_det']

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