Theorems · Theorem · linear algebra

Matrix.adjugate_submatrix_equiv_self

∀ {m : Type u} {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : Fintype m] [inst_4 : CommRing α] (e : n ≃ m) (A : Matrix m m α),
  (A.submatrix ⇑e ⇑e).adjugate = A.adjugate.submatrix ⇑e ⇑e

Defined in

Mathlib.LinearAlgebra.Matrix.Adjugate

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeDecidableEqFintypeCommRing