det_symm

Mathlib.LinearAlgebra.Determinant

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

English

Conjugating a linear equivalence by another linear equivalence does not change its determinant.

Русский

Сопряжение линейного эквивалента другим линейным эквивалентом не меняет детерминант.

LaTeX

$$$\det\bigl((e^{-1} \circ f \circ e)\bigr) = \det f$$$

Lean4

@[simp]
theorem det_symm (f : M ≃ₗ[R] M) : LinearEquiv.det f.symm = LinearEquiv.det f⁻¹ :=
  map_inv _ f

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

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

Разделы

Аффилиация

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