Theorems · Theorem · linear algebra

Matrix.det_unique

∀ {R : Type v} [inst : CommRing R] {n : Type u_3} [inst_1 : Unique n] [inst_2 : DecidableEq n] [inst_3 : Fintype n]
  (A : Matrix n n R), A.det = A default default

If n has only one element, the determinant of an n by n matrix is just that element. Although Unique implies DecidableEq and Fintype, the instances might not be syntactically equal. Thus, we need to fill in the args explicitly.

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

15 results in Mathlib

Foundations

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

Assumes

CommRingUniqueDecidableEqFintype