Determinant of families of vectors #
This file defines the determinant of an endomorphism, and of a family of vectors
with respect to some basis. For the determinant of a matrix, see the file
Main definitions #
In the list below, and in all this file,
R is a commutative ring (semiring
is sometimes enough),
M and its variations are
m are finite
types used for indexing.
basis.det: the determinant of a family of vectors with respect to a basis, as a multilinear map
linear_map.det: the determinant of an endomorphism
f : End R Mas a multiplicative homomorphism (if
Mdoes not have a finite
R-basis, the result is
basis, det, determinant
R^n are linearly equivalent, then
n are also equivalent.
M' are each other's inverse matrices, they are square matrices up to
equivalence of types.
M' is a two-sided inverse for
M (indexed differently),
det (M ⬝ N ⬝ M') = det N.
Determinant of a linear map #
The determinant of
linear_map.to_matrix does not depend on the choice of basis.
The determinant of an endomorphism given a basis.
linear_map.det for a version that populates the basis non-computably.
trunc (basis ι A M) parameter makes it slightly more convenient to switch bases,
there is no good way to generalize over universe parameters, so we can't fully state in
type that it does not depend on the choice of basis. Instead you can use the
or avoid mentioning a basis at all using
Unfold lemma for
det_aux_def' which allows you to vary the basis.
The determinant of an endomorphism independent of basis.
If there is no finite basis on
M, the result is
P f.det it suffices to consider
P (to_matrix _ _ f).det and
Builds a linear equivalence from a linear map whose determinant in some bases is a unit.
The determinant of a family of vectors with respect to some basis, as an alternating multilinear map.