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
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_6}
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 := _}
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 := _, add_comm := _, mul := monoid.mul matrix.monoid, mul_assoc := _, one := monoid.one matrix.monoid, one_mul := _, mul_one := _, 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 := _, 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 := _, 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.
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 correspnding "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 correspnding "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 correspnding "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 correspnding "bottom right" submatrix.
Equations
- M.to_blocks₂₂ = λ (i : o) (j : m), M (sum.inr i) (sum.inr j)
matrix.block_diagonal M
turns M : o → matrix m n α'
into a
m × o
-byn × o
block matrix which has the entries of M
along the diagonal
and zero elsewhere.
Equations
- matrix.block_diagonal M (i, k) (j, k') = ite (k = k') (M k i j) 0