det_eq_elem_of_subsingleton — Mathlib

English

If the set of indices is a singleton, the determinant equals the single entry on the diagonal.

Русский

Если множество индексов содержит единственный элемент, детерминант равен единственному элементу на диагонали.

LaTeX

$$$\\det A = A_{kk}$ when $n$ is singleton$$

Lean4

theorem det_eq_elem_of_subsingleton [Subsingleton n] (A : Matrix n n R) (k : n) : det A = A k k :=
  by
  have := uniqueOfSubsingleton k
  convert det_unique A

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