Matrices #
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
The add_monoid_hom
between spaces of matrices induced by an add_monoid_hom
between their
coefficients.
diagonal d
is the square matrix such that (diagonal d) i i = d i
and (diagonal d) i j = 0
if i ≠ j
.
Equations
- matrix.diagonal d = λ (i j : n), ite (i = j) (d i) 0
Equations
- matrix.has_one = {one := matrix.diagonal (λ (_x : n), 1)}
dot_product v w
is the sum of the entrywise products v i * w i
Equations
- matrix.dot_product v w = ∑ (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 Ǹ
.
Equations
- M ⬝ 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_8}
Equations
- matrix.semigroup = {mul := has_mul.mul matrix.has_mul, mul_assoc := _}
Equations
- matrix.monoid = {mul := semigroup.mul matrix.semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (matrix n n α)), npow_zero' := _, npow_succ' := _}
Equations
- matrix.semiring = {add := add_comm_monoid.add matrix.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero matrix.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul matrix.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := monoid.mul matrix.monoid, mul_assoc := _, one := monoid.one matrix.monoid, one_mul := _, mul_one := _, npow := npow matrix.monoid, npow_zero' := _, npow_succ' := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}
A version of one_map
where f
is a ring hom.
A version of one_map
where f
is a ring_equiv
.
A version of map_zero
where f
is a add_monoid_hom
.
A version of map_zero
where f
is a add_equiv
.
A version of map_zero
where f
is a linear_map
.
A version of map_zero
where f
is a linear_equiv
.
A version of map_zero
where f
is a ring_equiv
.
The ring_hom
between spaces of square matrices induced by a ring_hom
between their
coefficients.
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 := _, add_left_neg := _, add_comm := _, mul := semiring.mul matrix.semiring, mul_assoc := _, one := semiring.one matrix.semiring, one_mul := _, mul_one := _, npow := semiring.npow matrix.semiring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
Equations
Equations
- matrix.semimodule = pi.semimodule m (λ (ᾰ : m), n → β) α
The ring homomorphism α →+* matrix n n α
sending a
to the diagonal matrix with a
on the diagonal.
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)
std_basis_matrix i j a
is the matrix with a
in the i
-th row, j
-th column,
and zeroes elsewhere.
When R
is a *
-(semi)ring, matrix n n R
becomes a *
-(semi)ring with
the star operation given by taking the conjugate, and the star of each entry.
Equations
- matrix.star_ring = {to_star_monoid := {to_has_involutive_star := {to_has_star := {star := λ (M : matrix n n R), Mᵀ.map star}, star_involutive := _}, star_mul := _}, star_add := _}
M.minor row col
is the matrix obtained by reindexing the rows and the lines of
M
, such that M.minor row col i j = M (row i) (col j)
. Note that the total number
of row/colums doesn't have to be preserved.
If the minor doesn't repeat elements, then when applied to a diagonal matrix the result is diagonal.
simp
lemmas for matrix.minor
s interaction with matrix.diagonal
, 1
, and matrix.mul
for
when the mappings are bundled.
row_col
section #
Simplification lemmas for matrix.row
and matrix.col
.
Update, i.e. replace the i
th row of matrix A
with the values in b
.
Equations
- M.update_row i b = function.update M i b
Update, i.e. replace the j
th column of matrix A
with the values in b
.
Equations
- M.update_column j b = λ (i : n), function.update (M i) j (b i)
We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.
Equations
- A.from_blocks B C D = sum.elim (λ (i : n), sum.elim (A i) (B i)) (λ (i : o), sum.elim (C i) (D i))
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.
Equations
- M.to_blocks₁₁ = λ (i : n) (j : l), M (sum.inl i) (sum.inl j)
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.
Equations
- M.to_blocks₁₂ = λ (i : n) (j : m), M (sum.inl i) (sum.inr j)
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.
Equations
- M.to_blocks₂₁ = λ (i : o) (j : l), M (sum.inr i) (sum.inl j)
Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.
Equations
- M.to_blocks₂₂ = λ (i : o) (j : m), M (sum.inr i) (sum.inr j)
Let p
pick out certain rows and q
pick out certain columns of a matrix M
. Then
to_block M p q
is the corresponding block matrix.
Alternate version with b : m → nat
. Let b
map rows and columns of a square matrix M
to
blocks. Then to_square_block' M b k
is the block k
matrix.
Equations
- M.to_square_block' b k = M.minor coe coe
Let p
pick out certain rows and columns of a square matrix M
. Then
to_square_block_prop M p
is the corresponding block matrix.
Equations
- M.to_square_block_prop p = M.minor coe coe
matrix.block_diagonal M
turns a homogenously-indexed collection of matrices
M : o → matrix m n α'
into a m × o
-by-n × o
block matrix which has the entries of M
along
the diagonal and zero elsewhere.
See also matrix.block_diagonal'
if the matrices may not have the same size everywhere.
Equations
- matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0
matrix.block_diagonal' M
turns M : Π i, matrix (m i) (n i) α
into a
Σ i, m i
-by-Σ i, n i
block matrix which has the entries of M
along the diagonal
and zero elsewhere.
This is the dependently-typed version of matrix.block_diagonal
.