det_eq_elem_of_card_eq_one — Mathlib

English

If the index type is subsingleton, det A equals the diagonal element here.

Русский

Если тип индексов подсвязанный, det A равен диагональному элементу.

LaTeX

$$[Subsingleton n] (A : Matrix n n R) (k : n), det A = A_{kk}$$

Lean4

theorem det_eq_elem_of_card_eq_one {A : Matrix n n R} (h : Fintype.card n = 1) (k : n) : det A = A k k :=
  haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le
  det_eq_elem_of_subsingleton _ _

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