det_inv

Mathlib.LinearAlgebra.Determinant

URI: https://scilib.ai/kg/mathlib#Module.Basis.det_inv

← MathLib Explorer

English

Same principle: the inverse of det(b,b') equals det(b',b).

Русский

То же самое: обратное к det(b,b') равно det(b',b).

LaTeX

$$det(b',b) = (det(b,b'))^{-1}$$

Lean4

theorem det_inv (b : Basis ι A M) (b' : Basis ι A M) : (b.isUnit_det b').unit⁻¹ = b'.det b :=
  by
  rw [← Units.mul_eq_one_iff_inv_eq, IsUnit.unit_spec, ← det_basis, ← det_basis]
  exact LinearEquiv.det_mul_det_symm _

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

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

Разделы

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

Аффилиация

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