det_coe_symm — Mathlib

English

For a linear bijection A, the determinant of its inverse equals the reciprocal of the determinant of A.

Русский

Для линейного взаимно однозначного отображения A определитель его обратного отображения равен дроби 1/детерминант(A).

LaTeX

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

Lean4

@[simp]
theorem det_coe_symm {R : Type*} [Field R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] [Module R M]
    (A : M ≃L[R] M) : (A.symm : M →L[R] M).det = (A : M →L[R] M).det⁻¹ :=
  LinearEquiv.det_coe_symm A.toLinearEquiv

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