det_symm_mul_det — Mathlib

English

Given a linear map f: N → M and equivalences e,e': M ≃ N, the determinants of f∘e and f∘e' are associated.

Русский

Детерминанты отображений f∘e и f∘e' ассоциированы.

LaTeX

$$Associated( det(f ∘ e), det(f ∘ e') )$$

Lean4

/-- The determinants of a `LinearEquiv` and its inverse multiply to 1. -/
@[simp]
theorem det_symm_mul_det {A : Type*} [CommRing A] [Module A M] (f : M ≃ₗ[A] M) :
    LinearMap.det (f.symm : M →ₗ[A] M) * LinearMap.det (f : M →ₗ[A] M) = 1 := by
  simp [← LinearMap.det_comp]
    -- Cannot be stated using `LinearMap.det` because `f` is not an endomorphism.

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