Extensive documentation in the header of:
(Credits ITP 2013 tutorial: The Mathematical Components library
by Enrico Tassi and Assia Mahboubi)
Some notations : size inside parentheses, type of coefficients inside square brackets. NB: In the library, the type of coefficients can also be ommitted.
The type matrix
is just a tag over ffun: it inherits from its structure.
We can transfer
automatically all structures from the type of finite
functions by trivial subTyping
.
Test overloaded "_ == _" notation
Since matrices over nat are comparable with _ == _, matrices over matrices over nat are also comparable
We define a coercion in order to access elements as if matrices were functions.
We provide a notation to build matrices from a general term.
We now show the most used theorems for matrix manipulation.
mxE is an equation to compute a term in the matrix at given coordinates: it extracts the general term of the matrix and compute the substitution of indexes. It is generally the right move when you have
(A complicated matrix) i j
in your goal.
matrixP is the extensionality theorem
for matrices, it says two
matrices are equal if and only if all their coefficients are pairwise
equal.
(do not confuse the names)
But not a ring as the multiplication is heterogeneous.
This ring product coincides with the matrix product.
and these notions of inversibility are definitionally equivalent.
u *m A
Alternatively, the library provides an equivalent definition (via eqmxP) that can be used for rewriting in inclusion statements or rank.