det_neg

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

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

English

Let A be an n×n matrix. Then det(-A) = (-1)^n det(A).

Русский

Пусть A — матрица размера n×n. Тогда det(-A) = (-1)^n det(A).

LaTeX

$$$$\det(-A) = (-1)^{n} \det A,$$ где $n = Fintype.card\, n$.$$

Lean4

theorem det_neg (A : Matrix n n R) : det (-A) = (-1) ^ Fintype.card n * det A := by rw [← det_smul, neg_one_smul]

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

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

Разделы

Аффилиация

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