det_taylorLinearEquiv — Mathlib

English

Let R be a commutative ring. The determinant of the Taylor linear equivalence (viewed as a linear map) is 1.

Русский

Пусть R — коммутативное кольцо. Детерминант линейного отображения Тейлора равен 1.

LaTeX

$$$\det\bigl((taylorLinearEquiv\, r\, n)\bigr) = 1$$$

Lean4

@[simp]
theorem det_taylorLinearEquiv : (taylorLinearEquiv r n).det = 1 :=
  Units.ext <| by rw [LinearEquiv.coe_det, det_taylorLinearEquiv_toLinearMap, Units.val_one]

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