det_fin_one

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.det_fin_one

English

Determinant of a 1×1 matrix is its single entry.

Русский

Детерминант матрицы размером 1×1 равен её единственному элементу.

LaTeX

$$$\\det A = A_{00} \\quad\\text{for } A \\in M(\\mathrm{Fin} 1, \\mathrm{Fin} 1, R)$$$

Lean4

/-- Determinant of 1x1 matrix -/
theorem det_fin_one (A : Matrix (Fin 1) (Fin 1) R) : det A = A 0 0 :=
  det_unique A

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru