det_unique — Mathlib

English

For a matrix of size n with a single element, the determinant equals that element.

Русский

Для матрицы размера n с одним элементом детерминант равен этому элементу.

LaTeX

$$$\\det A = A_{kk}$ when $|n|=1$$$

Lean4

/-- 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. -/
@[simp]
theorem det_unique {n : Type*} [Unique n] [DecidableEq n] [Fintype n] (A : Matrix n n R) : det A = A default default :=
  by simp [det_apply, univ_unique]

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