Theorems · Theorem · linear algebra

Matrix.mul_adjp_apply_ne

∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  (i j : n), i ≠ j → (A * Matrix.adjp 1 A) i j = (A * Matrix.adjp (-1) A) i j

Defined in

Mathlib.LinearAlgebra.Matrix.SemiringInverse

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqCommSemiring