Theorems · Theorem · linear algebra

Matrix.det_fin_three

∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 3) (Fin 3) R),
  A.det =
    A 0 0 * A 1 1 * A 2 2 - A 0 0 * A 1 2 * A 2 1 - A 0 1 * A 1 0 * A 2 2 + A 0 1 * A 1 2 * A 2 0 +
        A 0 2 * A 1 0 * A 2 1 -
      A 0 2 * A 1 1 * A 2 0

Determinant of 3x3 matrix

Defined in

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRing