det_fin_two — Mathlib

English

Determinant of a 2×2 matrix is ad − bc.

Русский

Детерминант матрицы 2×2 равен ad − bc.

LaTeX

$$$\\det A = A_{00} A_{11} - A_{01} A_{10}$$$

Lean4

/-- Determinant of 2x2 matrix -/
theorem det_fin_two (A : Matrix (Fin 2) (Fin 2) R) : det A = A 0 0 * A 1 1 - A 0 1 * A 1 0 :=
  by
  simp only [det_succ_row_zero, det_unique, Fin.default_eq_zero, submatrix_apply, Fin.succ_zero_eq_one,
    Fin.sum_univ_succ, Fin.val_zero, Fin.zero_succAbove, univ_unique, Fin.val_succ, Fin.val_eq_zero,
    Fin.succ_succAbove_zero, sum_singleton]
  ring

Похожие утверждения