detRowAlternating — Mathlib

English

The determinant is an alternating multilinear map in the rows of a matrix.

Русский

Детерминант является чередующейся многочленной формой по строкам матрицы.

LaTeX

$$$\\detRowAlternating : (n \\to R) [\\\,⋀^n]\\to_ℓ[R] R$$$

Lean4

/-- `det` is an `AlternatingMap` in the rows of the matrix. -/
def detRowAlternating : (n → R) [⋀^n]→ₗ[R] R :=
  MultilinearMap.alternatization ((MultilinearMap.mkPiAlgebra R n R).compLinearMap LinearMap.proj)

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