Matrix and vector notation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file includes
simp lemmas for applying operations in
data.matrix.basic to values built out
of the matrix notation
![a, b] = vec_cons a (vec_cons b vec_empty) defined in
Implementation notes #
simp lemmas require that one of the arguments is of the form
vec_cons _ _.
simp works with entries only when (some) entries are already given.
In other words, this notation will only appear in the output of
simp if it
already appears in the input.
This file provide notation
!![a, b; c, d] for matrices, which corresponds to
matrix.of ![![a, b], ![c, d]].
A parser for
a, b; c, d-style strings is provided as
matrix.notation provides the hook for the
Note that in lean 3 the pretty-printer will not show
!! notation, instead showing the version
Examples of usage can be found in the
![...] notation for displaying a
fin-indexed matrix, for example:
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6] -- !![4, 6; 8, 10]
Updating a row then removing it is the same as removing it.
Updating a column then removing it is the same as removing it.