det_refl

Mathlib.LinearAlgebra.Determinant

URI: https://scilib.ai/kg/mathlib#LinearEquiv.det_refl

English

The determinant of a linear equivalence times the determinant of its inverse equals 1: det f · det f⁻¹ = 1.

Русский

Детерминант линейного эквивалента, умноженный на детерминант его обратного, равен 1.

LaTeX

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

Lean4

@[simp]
theorem det_refl : LinearEquiv.det (LinearEquiv.refl R M) = 1 :=
  Units.ext <| LinearMap.det_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru