det_conj'

Mathlib.LinearAlgebra.Matrix.NonsingularInverse

URI: https://scilib.ai/kg/mathlib#Matrix.det_conj'

← MathLib Explorer

English

A variant of det_units_conj': det(M^{-1} N M) = det N when M is a unit.

Русский

Вариант det_units_conj': det(M^{-1} N M) = det N при единице M.

LaTeX

$$det (M^{-1} * N * M) = det N$$

Lean4

/-- A variant of `Matrix.det_units_conj'`. -/
theorem det_conj' {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M⁻¹ * N * M) = det N := by
  rw [← h.unit_spec, ← coe_units_inv, det_units_conj']

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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