det — Mathlib

English

The determinant equals the sum over all permutations of the sign of the permutation times the product of matrix entries along the permutation.

Русский

Детерминант равен сумме по всем перестановкам знака перестановки и произведения соответствующих элементов матрицы.

LaTeX

$$$\\det(M) = \\sum_{\\sigma \\in \\mathrm{Perm}(n)} \\mathrm{sign}(\\sigma) \\prod_i M(\\sigma(i), i)$$$

Lean4

/-- The determinant of a matrix given by the Leibniz formula. -/
abbrev det (M : Matrix n n R) : R :=
  detRowAlternating M

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