det_mul_det_symm — Mathlib

English

The determinants of a linear equivalence and its inverse multiply to 1.

Русский

Детерминанты линейного эквивалента и его обращения перемножаются в единицу.

LaTeX

$$$\det f \cdot \det f^{-1} = 1$$$

Lean4

/-- The determinants of a `LinearEquiv` and its inverse multiply to 1. -/
@[simp]
theorem det_mul_det_symm {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f : M →ₗ[A] M) * LinearMap.det (f.symm : M →ₗ[A] M) = 1 := by simp [← LinearMap.det_comp]

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