Matrices #
This file defines basic properties of matrices.
Matrices with rows indexed by m
, columns indexed by n
, and entries of type α
are represented
with matrix m n α
. For the typical approach of counting rows and columns,
matrix (fin m) (fin n) α
can be used.
Notation #
The locale matrix
gives the following notation:
⬝ᵥ
formatrix.dot_product
⬝
formatrix.mul
ᵀ
formatrix.transpose
ᴴ
formatrix.conj_transpose
Implementation notes #
For convenience, matrix m n α
is defined as m → n → α
, as this allows elements of the matrix
to be accessed with A i j
. However, it is not advisable to construct matrices using terms of the
form λ i j, _
or even (λ i j, _ : matrix m n α)
, as these are not recognized by lean as having
the right type. Instead, matrix.of
should be used.
TODO #
Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.
matrix m n R
is the type of matrices with entries in R
, whose rows are indexed by m
and whose columns are indexed by n
.
Instances for matrix
- matrix.inhabited
- matrix.has_add
- matrix.add_semigroup
- matrix.add_comm_semigroup
- matrix.has_zero
- matrix.add_zero_class
- matrix.add_monoid
- matrix.add_comm_monoid
- matrix.has_neg
- matrix.has_sub
- matrix.add_group
- matrix.add_comm_group
- matrix.unique
- matrix.subsingleton
- matrix.nontrivial
- matrix.has_smul
- matrix.smul_comm_class
- matrix.is_scalar_tower
- matrix.is_central_scalar
- matrix.mul_action
- matrix.distrib_mul_action
- matrix.module
- matrix.subsingleton_of_empty_left
- matrix.subsingleton_of_empty_right
- matrix.has_one
- matrix.has_mul
- matrix.non_unital_non_assoc_semiring
- matrix.semiring.is_scalar_tower
- matrix.semiring.smul_comm_class
- matrix.non_assoc_semiring
- matrix.non_unital_semiring
- matrix.semiring
- matrix.non_unital_non_assoc_ring
- matrix.non_unital_ring
- matrix.non_assoc_ring
- matrix.ring
- matrix.algebra
- matrix.has_star
- matrix.has_involutive_star
- matrix.star_add_monoid
- matrix.star_ring
- matrix.matrix.reflect
- matrix.has_repr
- matrix.finite_dimensional
- matrix.fintype
- matrix.has_inv
- module.free.matrix
- module.finite.matrix
- matrix.topological_space
- matrix.t2_space
- matrix.has_continuous_const_smul
- matrix.has_continuous_smul
- matrix.has_continuous_add
- matrix.has_continuous_neg
- matrix.topological_add_group
- matrix.has_continuous_star
- matrix.has_continuous_mul
- matrix.topological_semiring
- matrix.topological_ring
- matrix.special_linear_group.has_coe_to_matrix
- matrix.normed_star_group
- matrix.norm_one_class
- matrix.linfty_op_norm_one_class
- matrix.frobenius_normed_star_group
- matrix.div_inv_monoid
- matrix.uniform_space
- matrix.complete_space
- matrix.separated_space
- matrix.unitary_group.coe_matrix
- matrix.char_p
Cast a function into a matrix.
The two sides of the equivalence are definitionally equal types. We want to use an explicit cast
to distinguish the types because matrix
has different instances to pi types (such as pi.has_mul
,
which performs elementwise multiplication, vs matrix.has_mul
).
If you are defining a matrix, in terms of its entries, either use of (λ i j, _)
, or use pattern
matching in a definition as | i j := _
(which can only be unfolded when fully-applied). The
purpose of this approach is to ensure that terms of the form (λ i j, _) * (λ i j, _)
do not
appear, as the type of *
can be misleading.
Equations
- matrix.of = equiv.refl (m → n → α)
M.map f
is the matrix obtained by applying f
to each entry of the matrix M
.
This is available in bundled forms as:
The transpose of a matrix.
Instances for matrix.transpose
The conjugate transpose of a matrix defined in term of star
.
Equations
matrix.col u
is the column matrix whose entries are given by u
.
Equations
- matrix.col w x y = w x
matrix.row u
is the row matrix whose entries are given by u
.
Equations
- matrix.row v x y = v y
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
Equations
- matrix.module = pi.module m (λ (ᾰ : m), n → α) R
simp-normal form pulls of
to the outside.
The scalar action via has_mul.to_has_smul
is transformed by the same map as the elements
of the matrix, when f
preserves multiplication.
The scalar action via has_mul.to_has_opposite_smul
is transformed by the same map as the
elements of the matrix, when f
preserves multiplication.
diagonal d
is the square matrix such that (diagonal d) i i = d i
and (diagonal d) i j = 0
if i ≠ j
.
Note that bundled versions exist as:
matrix.diagonal_add_monoid_hom
matrix.diagonal_linear_map
matrix.diagonal_ring_hom
matrix.diagonal_alg_hom
Equations
- matrix.diagonal d i j = ite (i = j) (d i) 0
matrix.diagonal
as an add_monoid_hom
.
Equations
- matrix.diagonal_add_monoid_hom n α = {to_fun := matrix.diagonal (add_zero_class.to_has_zero α), map_zero' := _, map_add' := _}
matrix.diagonal
as a linear_map
.
Equations
- matrix.diagonal_linear_map n R α = {to_fun := (matrix.diagonal_add_monoid_hom n α).to_fun, map_add' := _, map_smul' := _}
Equations
- matrix.has_one = {one := matrix.diagonal (λ (_x : n), 1)}
The diagonal of a square matrix.
matrix.diag
as an add_monoid_hom
.
Equations
- matrix.diag_add_monoid_hom n α = {to_fun := matrix.diag α, map_zero' := _, map_add' := _}
matrix.diag
as a linear_map
.
Equations
- matrix.diag_linear_map n R α = {to_fun := (matrix.diag_add_monoid_hom n α).to_fun, map_add' := _, map_smul' := _}
dot_product v w
is the sum of the entrywise products v i * w i
Equations
- matrix.dot_product v w = finset.univ.sum (λ (i : m), v i * w i)
M ⬝ N
is the usual product of matrices M
and N
, i.e. we have that
(M ⬝ N) i k
is the dot product of the i
-th row of M
by the k
-th column of N
.
This is currently only defined when m
is finite.
Equations
- M.mul N = λ (i : l) (k : n), matrix.dot_product (λ (j : m), M i j) (λ (j : m), N j k)
Equations
- matrix.has_mul = {mul := matrix.mul _inst_3}
Equations
- matrix.non_unital_non_assoc_semiring = {add := has_add.add matrix.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul matrix.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := has_mul.mul matrix.has_mul, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
Left multiplication by a matrix, as an add_monoid_hom
from matrices to matrices.
Right multiplication by a matrix, as an add_monoid_hom
from matrices to matrices.
This instance enables use with smul_mul_assoc
.
This instance enables use with mul_smul_comm
.
Equations
- matrix.non_assoc_semiring = {add := non_unital_non_assoc_semiring.add matrix.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero matrix.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul matrix.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul matrix.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := 1, one_mul := _, mul_one := _, nat_cast := λ (n_1 : ℕ), matrix.diagonal (λ (_x : n), ↑n_1), nat_cast_zero := _, nat_cast_succ := _}
matrix.diagonal
as a ring_hom
.
Equations
- matrix.diagonal_ring_hom n α = {to_fun := matrix.diagonal (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}
Equations
- matrix.non_unital_semiring = {add := non_unital_non_assoc_semiring.add matrix.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero matrix.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul matrix.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul matrix.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
Equations
- matrix.semiring = {add := non_unital_semiring.add matrix.non_unital_semiring, add_assoc := _, zero := non_unital_semiring.zero matrix.non_unital_semiring, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul matrix.non_unital_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_semiring.mul matrix.non_unital_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := non_assoc_semiring.one matrix.non_assoc_semiring, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast matrix.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := monoid_with_zero.npow._default non_assoc_semiring.one non_unital_semiring.mul matrix.semiring._proof_16 matrix.semiring._proof_17, npow_zero' := _, npow_succ' := _}
Equations
- matrix.non_unital_non_assoc_ring = {add := non_unital_non_assoc_semiring.add matrix.non_unital_non_assoc_semiring, add_assoc := _, zero := non_unital_non_assoc_semiring.zero matrix.non_unital_non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_unital_non_assoc_semiring.nsmul matrix.non_unital_non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg matrix.add_comm_group, sub := add_comm_group.sub matrix.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul matrix.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_non_assoc_semiring.mul matrix.non_unital_non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _}
Equations
- matrix.non_unital_ring = {add := non_unital_semiring.add matrix.non_unital_semiring, add_assoc := _, zero := non_unital_semiring.zero matrix.non_unital_semiring, zero_add := _, add_zero := _, nsmul := non_unital_semiring.nsmul matrix.non_unital_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg matrix.add_comm_group, sub := add_comm_group.sub matrix.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul matrix.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_unital_semiring.mul matrix.non_unital_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}
Equations
- matrix.non_assoc_ring = {add := non_assoc_semiring.add matrix.non_assoc_semiring, add_assoc := _, zero := non_assoc_semiring.zero matrix.non_assoc_semiring, zero_add := _, add_zero := _, nsmul := non_assoc_semiring.nsmul matrix.non_assoc_semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg matrix.add_comm_group, sub := add_comm_group.sub matrix.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul matrix.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := non_assoc_semiring.mul matrix.non_assoc_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := non_assoc_semiring.one matrix.non_assoc_semiring, one_mul := _, mul_one := _, nat_cast := non_assoc_semiring.nat_cast matrix.non_assoc_semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast := add_group_with_one.int_cast._default non_assoc_semiring.nat_cast non_assoc_semiring.add matrix.non_assoc_ring._proof_20 non_assoc_semiring.zero matrix.non_assoc_ring._proof_21 matrix.non_assoc_ring._proof_22 non_assoc_semiring.nsmul matrix.non_assoc_ring._proof_23 matrix.non_assoc_ring._proof_24 non_assoc_semiring.one matrix.non_assoc_ring._proof_25 matrix.non_assoc_ring._proof_26 add_comm_group.neg add_comm_group.sub matrix.non_assoc_ring._proof_27 add_comm_group.zsmul matrix.non_assoc_ring._proof_28 matrix.non_assoc_ring._proof_29 matrix.non_assoc_ring._proof_30 matrix.non_assoc_ring._proof_31, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
Equations
- matrix.ring = {add := semiring.add matrix.semiring, add_assoc := _, zero := semiring.zero matrix.semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul matrix.semiring, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg matrix.add_comm_group, sub := add_comm_group.sub matrix.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul matrix.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_comm_group_with_one.int_cast._default semiring.nat_cast semiring.add matrix.ring._proof_12 semiring.zero matrix.ring._proof_13 matrix.ring._proof_14 semiring.nsmul matrix.ring._proof_15 matrix.ring._proof_16 semiring.one matrix.ring._proof_17 matrix.ring._proof_18 add_comm_group.neg add_comm_group.sub matrix.ring._proof_19 add_comm_group.zsmul matrix.ring._proof_20 matrix.ring._proof_21 matrix.ring._proof_22 matrix.ring._proof_23, nat_cast := semiring.nat_cast matrix.semiring, one := semiring.one matrix.semiring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := semiring.mul matrix.semiring, mul_assoc := _, one_mul := _, mul_one := _, npow := semiring.npow matrix.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
The ring homomorphism α →+* matrix n n α
sending a
to the diagonal matrix with a
on the diagonal.
Equations
- matrix.algebra = {to_has_smul := matrix.has_smul smul_with_zero.to_has_smul, to_ring_hom := {to_fun := ((matrix.scalar n).comp (algebra_map R α)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
matrix.diagonal
as an alg_hom
.
Equations
- matrix.diagonal_alg_hom R = {to_fun := matrix.diagonal (mul_zero_class.to_has_zero α), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
Bundled versions of matrix.map
#
The equiv
between spaces of matrices induced by an equiv
between their
coefficients. This is matrix.map
as an equiv
.
The add_monoid_hom
between spaces of matrices induced by an add_monoid_hom
between their
coefficients. This is matrix.map
as an add_monoid_hom
.
The add_equiv
between spaces of matrices induced by an add_equiv
between their
coefficients. This is matrix.map
as an add_equiv
.
The linear_map
between spaces of matrices induced by a linear_map
between their
coefficients. This is matrix.map
as a linear_map
.
The linear_equiv
between spaces of matrices induced by an linear_equiv
between their
coefficients. This is matrix.map
as an linear_equiv
.
The ring_hom
between spaces of square matrices induced by a ring_hom
between their
coefficients. This is matrix.map
as a ring_hom
.
The ring_equiv
between spaces of square matrices induced by a ring_equiv
between their
coefficients. This is matrix.map
as a ring_equiv
.
The alg_hom
between spaces of square matrices induced by a alg_hom
between their
coefficients. This is matrix.map
as a alg_hom
.
The alg_equiv
between spaces of square matrices induced by a alg_equiv
between their
coefficients. This is matrix.map
as a alg_equiv
.
For two vectors w
and v
, vec_mul_vec w v i j
is defined to be w i * v j
.
Put another way, vec_mul_vec w v
is exactly col w ⬝ row v
.
Equations
- matrix.vec_mul_vec w v x y = w x * v y
mul_vec M v
is the matrix-vector product of M
and v
, where v
is seen as a column matrix.
Put another way, mul_vec M v
is the vector whose entries
are those of M ⬝ col v
(see col_mul_vec
).
Equations
- M.mul_vec v i = matrix.dot_product (λ (j : n), M i j) v
vec_mul v M
is the vector-matrix product of v
and M
, where v
is seen as a row matrix.
Put another way, vec_mul v M
is the vector whose entries
are those of row v ⬝ M
(see row_vec_mul
).
Equations
- matrix.vec_mul v M j = matrix.dot_product v (λ (i : m), M i j)
Left multiplication by a matrix, as an add_monoid_hom
from vectors to vectors.
Associate the dot product of mul_vec
to the left.
Tell simp
what the entries are in a transposed matrix.
Compare with mul_apply
, diagonal_apply_eq
, etc.
matrix.transpose
as an add_equiv
Equations
- matrix.transpose_add_equiv m n α = {to_fun := matrix.transpose α, inv_fun := matrix.transpose α, left_inv := _, right_inv := _, map_add' := _}
matrix.transpose
as a linear_map
Equations
- matrix.transpose_linear_equiv m n R α = {to_fun := (matrix.transpose_add_equiv m n α).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.transpose_add_equiv m n α).inv_fun, left_inv := _, right_inv := _}
matrix.transpose
as a ring_equiv
to the opposite ring
matrix.transpose
as an alg_equiv
to the opposite ring
Equations
- matrix.transpose_alg_equiv m R α = {to_fun := λ (M : matrix m m α), mul_opposite.op M.transpose, inv_fun := ((matrix.transpose_add_equiv m m α).trans mul_opposite.op_add_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
Tell simp
what the entries are in a conjugate transposed matrix.
Compare with mul_apply
, diagonal_apply_eq
, etc.
Note that star_module
is quite a strong requirement; as such we also provide the following
variants which this lemma would not apply to:
matrix.conj_transpose_smul_non_comm
matrix.conj_transpose_nsmul
matrix.conj_transpose_zsmul
matrix.conj_transpose_nat_cast_smul
matrix.conj_transpose_int_cast_smul
matrix.conj_transpose_inv_nat_cast_smul
matrix.conj_transpose_inv_int_cast_smul
matrix.conj_transpose_rat_smul
matrix.conj_transpose_rat_cast_smul
matrix.conj_transpose
as an add_equiv
Equations
matrix.conj_transpose
as a linear_map
Equations
- matrix.conj_transpose_linear_equiv m n R α = {to_fun := (matrix.conj_transpose_add_equiv m n α).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.conj_transpose_add_equiv m n α).inv_fun, left_inv := _, right_inv := _}
matrix.conj_transpose
as a ring_equiv
to the opposite ring
Equations
- matrix.conj_transpose_ring_equiv m α = {to_fun := λ (M : matrix m m α), mul_opposite.op M.conj_transpose, inv_fun := λ (M : (matrix m m α)ᵐᵒᵖ), (mul_opposite.unop M).conj_transpose, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
When α
has a star operation, square matrices matrix n n α
have a star
operation equal to matrix.conj_transpose
.
Equations
- matrix.has_star = {star := matrix.conj_transpose _inst_1}
Equations
When α
is a *
-additive monoid, matrix.has_star
is also a *
-additive monoid.
When α
is a *
-(semi)ring, matrix.has_star
is also a *
-(semi)ring.
Equations
A version of star_mul
for ⬝
instead of *
.
Given maps (r_reindex : l → m)
and (c_reindex : o → n)
reindexing the rows and columns of
a matrix M : matrix m n α
, the matrix M.submatrix r_reindex c_reindex : matrix l o α
is defined
by (M.submatrix r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j)
for (i,j) : l × o
.
Note that the total number of row and columns does not have to be preserved.