det_apply'

Mathlib.LinearAlgebra.Matrix.Determinant.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.det_apply'

English

The determinant can be expressed as the difference of two detp evaluations at +1 and -1.

Русский

Детерминант можно выразить как разность двух величин detp на +1 и -1.

LaTeX

$$$\\det(M) = \\detp(1; M) - \\detp(-1; M)$$$

Lean4

theorem det_apply' (M : Matrix n n R) : M.det = ∑ σ : Perm n, ε σ * ∏ i, M (σ i) i := by
  simp [det_apply, Units.smul_def]

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

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

Разделы

Аффилиация

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