Theorems · Theorem · linear algebra

Matrix.detp_mul

∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  (A B : Matrix n n R),
  Matrix.detp 1 (A * B) + (Matrix.detp 1 A * Matrix.detp (-1) B + Matrix.detp (-1) A * Matrix.detp 1 B) =
    Matrix.detp (-1) (A * B) + (Matrix.detp 1 A * Matrix.detp 1 B + Matrix.detp (-1) A * Matrix.detp (-1) B)

Defined in

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommSemiring