Theorems · Theorem · linear algebra

Matrix.det_conj_of_mul_eq_one

∀ {A : Type u_5} [inst : CommRing A] {m : Type u_6} {n : Type u_7} [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} {N : Matrix n n A},
  M * M' = 1 → M' * M = 1 → (M * N * M').det = N.det

If M' is a two-sided inverse for M (indexed differently), det (M * N * M') = det N. See Matrix.det_conj and Matrix.det_conj' for the case when M' = M⁻¹ or vice versa.

Defined in

Mathlib.LinearAlgebra.Determinant

Cited by

2 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFintypeFintypeDecidableEqDecidableEq