coe_ofIsUnitDet — Mathlib

English

The linear map corresponding to the constructed equivalence equals the original map when det is a unit.

Русский

Линейное отображение, содержащее эквивалентность, совпадает с исходной картой, еслиDet единична.

LaTeX

$$$(LinearEquiv.ofIsUnitDet h) = f$$$

Lean4

@[simp]
theorem coe_ofIsUnitDet {f : M →ₗ[R] M'} {v : Basis ι R M} {v' : Basis ι R M'}
    (h : IsUnit (LinearMap.toMatrix v v' f).det) : (LinearEquiv.ofIsUnitDet h : M →ₗ[R] M') = f :=
  by
  ext x
  rfl

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