# Linear algebra in mathematical components

Extensive documentation in the header of:

• definition of matrices
• main theorems
• help with depend types
• vector spaces as matrices

# Defining Matrices

(Credits ITP 2013 tutorial: The Mathematical Components library by Enrico Tassi and Assia Mahboubi material here)

## A matrix is a 2-dimension array

Some notations : size inside parentheses, type of coefficients inside square brackets. NB: In the library, the type of coefficients can also be ommitted.

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.

# Main Theorems

We now show the most used theorems for matrix manipulation.

## mxE

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`

## matrixP

matrixP is the extensionality theorem for matrices, it says two matrices are equal if and only if all their coefficients are pairwise equal.

## operations on matrices

### specific operation: trace and transpose

(do not confuse the names)

### matrices on rings are provided with a R-module canonical structure.

But not a ring as the multiplication is heterogeneous.

### square matrices with explicit non zero size have a ring canonical structure.

This ring product coincides with the matrix product.

### square matrices on a commutative unit ring with explicit non zero size have a unit ring canonical structure.

and these notions of inversibility are definitionally equivalent.

# SUB VECTOR SPACES AS MATRICES

## General understanding

• A specificity of the mathematical components library is to allow to reason on matrices as if they represented their own image.

• The doc and the code are in mxalgebra)

• rows can be seen as vectors, and matrix can be seen as the familiy of its row vectors.

• WARNING Following the english convention (which is opposite to the french convention), composition/application of linear maps represented by matrices should be done left to right: applying A to u is
`u *m A`
.

• as a consequence, membership to a space is the same operation as comparison of spaces.

### Addition of subspaces is not the same thing as addition of matrices.

(In Coq: same notation, different scope)

### Equality of subspaces is double inclusion.

Alternatively, the library provides an equivalent definition (via eqmxP) that can be used for rewriting in inclusion statements or rank.

## Usage.

• Im A is represented by the matrix A itself.

• vectors of a space represented by the matrix A are linear combinations of the rows of A, which amount to making a product by an element (i.e. row of coefficients, or coordinates in the family generated by A) on the left.

• Ker A is represented by the square matrix kermx A.

Let's do an example together