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
@[instance]
def
matrix.inhabited
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[inhabited α] :
Equations
@[instance]
Equations
@[instance]
def
matrix.add_semigroup
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_semigroup α] :
add_semigroup (matrix m n α)
Equations
@[instance]
def
matrix.add_comm_semigroup
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_comm_semigroup α] :
add_comm_semigroup (matrix m n α)
Equations
@[instance]
def
matrix.has_zero
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[has_zero α] :
Equations
@[instance]
def
matrix.add_monoid
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_monoid α] :
add_monoid (matrix m n α)
Equations
@[instance]
def
matrix.add_comm_monoid
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_comm_monoid α] :
add_comm_monoid (matrix m n α)
Equations
@[instance]
Equations
@[instance]
Equations
@[instance]
def
matrix.add_group
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_group α] :
Equations
@[instance]
def
matrix.add_comm_group
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_comm_group α] :
add_comm_group (matrix m n α)
Equations
@[instance]
Equations
@[instance]
def
matrix.subsingleton
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[subsingleton α] :
subsingleton (matrix m n α)
@[instance]
def
matrix.nontrivial
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[nonempty m]
[nonempty n]
[nontrivial α] :
nontrivial (matrix m n α)
theorem
matrix.subsingleton_of_empty_left
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
(hm : ¬nonempty m) :
subsingleton (matrix m n α)
theorem
matrix.subsingleton_of_empty_right
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
(hn : ¬nonempty n) :
subsingleton (matrix m n α)
def
add_monoid_hom.map_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_monoid α]
{β : Type w}
[add_monoid β]
(f : α →+ β) :
The add_monoid_hom between spaces of matrices induced by an add_monoid_hom between their
coefficients.
@[simp]
theorem
add_monoid_hom.map_matrix_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[add_monoid α]
{β : Type w}
[add_monoid β]
(f : α →+ β)
(M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
def
matrix.diagonal
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
(d : n → α) :
matrix n n α
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
@[simp]
theorem
matrix.diagonal_apply_eq
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
{d : n → α}
(i : n) :
matrix.diagonal d i i = d i
@[simp]
theorem
matrix.diagonal_apply_ne
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
{d : n → α}
{i j : n}
(h : i ≠ j) :
matrix.diagonal d i j = 0
theorem
matrix.diagonal_apply_ne'
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
{d : n → α}
{i j : n}
(h : j ≠ i) :
matrix.diagonal d i j = 0
@[simp]
theorem
matrix.diagonal_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α] :
matrix.diagonal (λ (_x : n), 0) = 0
@[simp]
theorem
matrix.diagonal_transpose
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
(v : n → α) :
(matrix.diagonal v)ᵀ = matrix.diagonal v
@[simp]
theorem
matrix.diagonal_add
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[add_monoid α]
(d₁ d₂ : n → α) :
matrix.diagonal d₁ + matrix.diagonal d₂ = matrix.diagonal (λ (i : n), d₁ i + d₂ i)
@[simp]
theorem
matrix.diagonal_map
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
{β : Type w}
[has_zero α]
[has_zero β]
{f : α → β}
(h : f 0 = 0)
{d : n → α} :
(matrix.diagonal d).map f = matrix.diagonal (λ (m : n), f (d m))
@[instance]
def
matrix.has_one
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α] :
Equations
- matrix.has_one = {one := matrix.diagonal (λ (_x : n), 1)}
@[simp]
theorem
matrix.diagonal_one
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α] :
matrix.diagonal (λ (_x : n), 1) = 1
theorem
matrix.one_apply
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α]
{i j : n} :
@[simp]
theorem
matrix.one_apply_eq
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α]
(i : n) :
1 i i = 1
@[simp]
theorem
matrix.one_apply_ne
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α]
{i j : n} :
theorem
matrix.one_apply_ne'
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α]
{i j : n} :
theorem
matrix.bit1_apply
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[add_monoid α]
[has_one α]
(M : matrix n n α)
(i j : n) :
@[simp]
theorem
matrix.bit1_apply_eq
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[add_monoid α]
[has_one α]
(M : matrix n n α)
(i : n) :
@[simp]
theorem
matrix.bit1_apply_ne
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[add_monoid α]
[has_one α]
(M : matrix n n α)
{i j : n}
(h : i ≠ j) :
def
matrix.dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[has_mul α]
[add_comm_monoid α]
(v w : m → α) :
α
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
theorem
matrix.dot_product_assoc
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(u : m → α)
(v : m → n → α)
(w : n → α) :
matrix.dot_product (λ (j : n), matrix.dot_product u (λ (i : m), v i j)) w = matrix.dot_product u (λ (i : m), matrix.dot_product (v i) w)
theorem
matrix.dot_product_comm
{m : Type u_2}
[fintype m]
{α : Type v}
[comm_semiring α]
(v w : m → α) :
matrix.dot_product v w = matrix.dot_product w v
@[simp]
theorem
matrix.dot_product_punit
{α : Type v}
[add_comm_monoid α]
[has_mul α]
(v w : punit → α) :
matrix.dot_product v w = (v punit.star) * w punit.star
@[simp]
theorem
matrix.dot_product_zero
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v : m → α) :
matrix.dot_product v 0 = 0
@[simp]
theorem
matrix.dot_product_zero'
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v : m → α) :
matrix.dot_product v (λ (_x : m), 0) = 0
@[simp]
theorem
matrix.zero_dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v : m → α) :
matrix.dot_product 0 v = 0
@[simp]
theorem
matrix.zero_dot_product'
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v : m → α) :
matrix.dot_product (λ (_x : m), 0) v = 0
@[simp]
theorem
matrix.add_dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(u v w : m → α) :
matrix.dot_product (u + v) w = matrix.dot_product u w + matrix.dot_product v w
@[simp]
theorem
matrix.dot_product_add
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(u v w : m → α) :
matrix.dot_product u (v + w) = matrix.dot_product u v + matrix.dot_product u w
@[simp]
theorem
matrix.diagonal_dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[decidable_eq m]
[semiring α]
(v w : m → α)
(i : m) :
matrix.dot_product (matrix.diagonal v i) w = (v i) * w i
@[simp]
theorem
matrix.dot_product_diagonal
{m : Type u_2}
[fintype m]
{α : Type v}
[decidable_eq m]
[semiring α]
(v w : m → α)
(i : m) :
matrix.dot_product v (matrix.diagonal w i) = (v i) * w i
@[simp]
theorem
matrix.dot_product_diagonal'
{m : Type u_2}
[fintype m]
{α : Type v}
[decidable_eq m]
[semiring α]
(v w : m → α)
(i : m) :
matrix.dot_product v (λ (j : m), matrix.diagonal w j i) = (v i) * w i
@[simp]
theorem
matrix.neg_dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[ring α]
(v w : m → α) :
matrix.dot_product (-v) w = -matrix.dot_product v w
@[simp]
theorem
matrix.dot_product_neg
{m : Type u_2}
[fintype m]
{α : Type v}
[ring α]
(v w : m → α) :
matrix.dot_product v (-w) = -matrix.dot_product v w
@[simp]
theorem
matrix.smul_dot_product
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(x : α)
(v w : m → α) :
matrix.dot_product (x • v) w = x * matrix.dot_product v w
@[simp]
theorem
matrix.dot_product_smul
{m : Type u_2}
[fintype m]
{α : Type v}
[comm_semiring α]
(x : α)
(v w : m → α) :
matrix.dot_product v (x • w) = x * matrix.dot_product v w
def
matrix.mul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
[fintype l]
[fintype m]
[fintype n]
{α : Type v}
[has_mul α]
[add_comm_monoid α]
(M : matrix l m α)
(N : matrix m n α) :
matrix l n α
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)
@[instance]
Equations
- matrix.has_mul = {mul := matrix.mul _inst_8}
@[simp]
theorem
matrix.mul_eq_mul
{n : Type u_3}
[fintype n]
{α : Type v}
[has_mul α]
[add_comm_monoid α]
(M N : matrix n n α) :
theorem
matrix.mul_apply'
{n : Type u_3}
[fintype n]
{α : Type v}
[has_mul α]
[add_comm_monoid α]
{M N : matrix n n α}
{i k : n} :
(M ⬝ N) i k = matrix.dot_product (λ (j : n), M i j) (λ (j : n), N j k)
@[instance]
Equations
- matrix.semigroup = {mul := has_mul.mul matrix.has_mul, mul_assoc := _}
@[simp]
theorem
matrix.diagonal_neg
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[add_group α]
(d : n → α) :
-matrix.diagonal d = matrix.diagonal (λ (i : n), -d i)
@[simp]
theorem
matrix.diagonal_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
(d : m → α)
(M : matrix m n α)
(i : m)
(j : n) :
(matrix.diagonal d ⬝ M) i j = (d i) * M i j
@[simp]
theorem
matrix.mul_diagonal
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(d : n → α)
(M : matrix m n α)
(i : m)
(j : n) :
(M ⬝ matrix.diagonal d) i j = (M i j) * d j
@[simp]
theorem
matrix.one_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
(M : matrix m n α) :
@[simp]
theorem
matrix.mul_one
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(M : matrix m n α) :
@[instance]
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' := _}
@[instance]
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 := _}
@[simp]
theorem
matrix.diagonal_mul_diagonal
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(d₁ d₂ : n → α) :
matrix.diagonal d₁ ⬝ matrix.diagonal d₂ = matrix.diagonal (λ (i : n), (d₁ i) * d₂ i)
theorem
matrix.diagonal_mul_diagonal'
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(d₁ d₂ : n → α) :
(matrix.diagonal d₁) * matrix.diagonal d₂ = matrix.diagonal (λ (i : n), (d₁ i) * d₂ i)
@[simp]
theorem
matrix.ring_hom_map_one
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
{β : Type w}
[semiring β]
(f : α →+* β) :
A version of one_map where f is a ring hom.
@[simp]
theorem
matrix.ring_equiv_map_one
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
{β : Type w}
[semiring β]
(f : α ≃+* β) :
A version of one_map where f is a ring_equiv.
@[simp]
theorem
matrix.add_monoid_hom_map_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
{β : Type w}
[add_monoid β]
(f : α →+ β) :
A version of map_zero where f is a add_monoid_hom.
@[simp]
theorem
matrix.add_equiv_map_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
{β : Type w}
[add_monoid β]
(f : α ≃+ β) :
A version of map_zero where f is a add_equiv.
@[simp]
theorem
matrix.linear_map_map_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
{R : Type u_1}
[semiring R]
{β : Type w}
[add_comm_monoid β]
[semimodule R α]
[semimodule R β]
(f : α →ₗ[R] β) :
A version of map_zero where f is a linear_map.
@[simp]
theorem
matrix.linear_equiv_map_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
{R : Type u_1}
[semiring R]
{β : Type w}
[add_comm_monoid β]
[semimodule R α]
[semimodule R β]
(f : α ≃ₗ[R] β) :
A version of map_zero where f is a linear_equiv.
@[simp]
theorem
matrix.ring_equiv_map_zero
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
{β : Type w}
[semiring β]
(f : α ≃+* β) :
A version of map_zero where f is a ring_equiv.
theorem
matrix.is_add_monoid_hom_mul_left
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
[fintype l]
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix l m α) :
is_add_monoid_hom (λ (x : matrix m n α), M ⬝ x)
theorem
matrix.is_add_monoid_hom_mul_right
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
[fintype l]
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α) :
is_add_monoid_hom (λ (x : matrix l m α), x ⬝ M)
@[simp]
theorem
matrix.row_mul_col_apply
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v w : m → α)
(i j : unit) :
(matrix.row v ⬝ matrix.col w) i j = matrix.dot_product v w
def
ring_hom.map_matrix
{m : Type u_2}
[fintype m]
{α : Type v}
[decidable_eq m]
[semiring α]
{β : Type w}
[semiring β]
(f : α →+* β) :
The ring_hom between spaces of square matrices induced by a ring_hom between their
coefficients.
@[simp]
theorem
ring_hom.map_matrix_apply
{m : Type u_2}
[fintype m]
{α : Type v}
[decidable_eq m]
[semiring α]
{β : Type w}
[semiring β]
(f : α →+* β)
(M : matrix m m α) :
⇑(f.map_matrix) M = M.map ⇑f
@[instance]
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 := _}
@[instance]
def
matrix.has_scalar
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α] :
has_scalar α (matrix m n α)
Equations
@[instance]
def
matrix.semimodule
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{β : Type w}
[semiring α]
[add_comm_monoid β]
[semimodule α β] :
semimodule α (matrix m n β)
Equations
- matrix.semimodule = pi.semimodule m (λ (ᾰ : m), n → β) α
theorem
matrix.smul_eq_diagonal_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
(M : matrix m n α)
(a : α) :
a • M = matrix.diagonal (λ (_x : m), a) ⬝ M
The ring homomorphism α →+* matrix n n α
sending a to the diagonal matrix with a on the diagonal.
@[simp]
theorem
matrix.coe_scalar
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n] :
⇑(matrix.scalar n) = λ (a : α), a • 1
theorem
matrix.scalar_apply_eq
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(a : α)
(i : n) :
⇑(matrix.scalar n) a i i = a
theorem
matrix.scalar_apply_ne
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
(a : α)
(i j : n)
(h : i ≠ j) :
⇑(matrix.scalar n) a i j = 0
theorem
matrix.scalar_inj
{n : Type u_3}
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq n]
[nonempty n]
{r s : α} :
⇑(matrix.scalar n) r = ⇑(matrix.scalar n) s ↔ r = s
theorem
matrix.smul_eq_mul_diagonal
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[comm_semiring α]
[decidable_eq n]
(M : matrix m n α)
(a : α) :
a • M = M ⬝ matrix.diagonal (λ (_x : n), a)
theorem
matrix.scalar.commute
{n : Type u_3}
[fintype n]
{α : Type v}
[comm_semiring α]
[decidable_eq n]
(r : α)
(M : matrix n n α) :
commute (⇑(matrix.scalar n) r) M
def
matrix.vec_mul_vec
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(w : m → α)
(v : n → α) :
matrix m n α
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
def
matrix.mul_vec
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α)
(v : n → α) :
m → α
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
def
matrix.vec_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(v : m → α)
(M : matrix m n α) :
n → α
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)
@[instance]
def
matrix.mul_vec.is_add_monoid_hom_left
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(v : n → α) :
is_add_monoid_hom (λ (M : matrix m n α), M.mul_vec v)
theorem
matrix.mul_vec_diagonal
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq m]
(v w : m → α)
(x : m) :
(matrix.diagonal v).mul_vec w x = (v x) * w x
theorem
matrix.vec_mul_diagonal
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq m]
(v w : m → α)
(x : m) :
matrix.vec_mul v (matrix.diagonal w) x = (v x) * w x
@[simp]
theorem
matrix.mul_vec_one
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq m]
(v : m → α) :
@[simp]
theorem
matrix.vec_mul_one
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq m]
(v : m → α) :
matrix.vec_mul v 1 = v
@[simp]
theorem
matrix.vec_mul_zero
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(A : matrix m n α) :
matrix.vec_mul 0 A = 0
@[simp]
theorem
matrix.vec_mul_vec_mul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[semiring α]
(v : m → α)
(M : matrix m n α)
(N : matrix n o α) :
matrix.vec_mul (matrix.vec_mul v M) N = matrix.vec_mul v (M ⬝ N)
theorem
matrix.vec_mul_vec_eq
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(w : m → α)
(v : n → α) :
matrix.vec_mul_vec w v = matrix.col w ⬝ matrix.row v
def
matrix.std_basis_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
[decidable_eq n]
(i : m)
(j : n)
(a : α) :
matrix m n α
std_basis_matrix i j a is the matrix with a in the i-th row, j-th column,
and zeroes elsewhere.
@[simp]
theorem
matrix.smul_std_basis_matrix
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
[decidable_eq n]
(i : m)
(j : n)
(a b : α) :
b • matrix.std_basis_matrix i j a = matrix.std_basis_matrix i j (b • a)
@[simp]
theorem
matrix.std_basis_matrix_zero
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
[decidable_eq n]
(i : m)
(j : n) :
matrix.std_basis_matrix i j 0 = 0
theorem
matrix.std_basis_matrix_add
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
[decidable_eq n]
(i : m)
(j : n)
(a b : α) :
matrix.std_basis_matrix i j (a + b) = matrix.std_basis_matrix i j a + matrix.std_basis_matrix i j b
theorem
matrix.matrix_eq_sum_std_basis
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
[decidable_eq m]
[decidable_eq n]
(x : matrix n m α) :
x = ∑ (i : n) (j : m), matrix.std_basis_matrix i j (x i j)
theorem
matrix.std_basis_eq_basis_mul_basis
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
[decidable_eq m]
[decidable_eq n]
(i : m)
(j : n) :
matrix.std_basis_matrix i j 1 = matrix.vec_mul_vec (λ (i' : m), ite (i = i') 1 0) (λ (j' : n), ite (j = j') 1 0)
theorem
matrix.induction_on'
{n : Type u_3}
[fintype n]
[decidable_eq n]
{X : Type u_1}
[semiring X]
{M : matrix n n X → Prop}
(m : matrix n n X)
(h_zero : M 0)
(h_add : ∀ (p q : matrix n n X), M p → M q → M (p + q))
(h_std_basis : ∀ (i j : n) (x : X), M (matrix.std_basis_matrix i j x)) :
M m
theorem
matrix.induction_on
{n : Type u_3}
[fintype n]
[decidable_eq n]
[nonempty n]
{X : Type u_1}
[semiring X]
{M : matrix n n X → Prop}
(m : matrix n n X)
(h_add : ∀ (p q : matrix n n X), M p → M q → M (p + q))
(h_std_basis : ∀ (i j : n) (x : X), M (matrix.std_basis_matrix i j x)) :
M m
theorem
matrix.neg_vec_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[ring α]
(v : m → α)
(A : matrix m n α) :
matrix.vec_mul (-v) A = -matrix.vec_mul v A
theorem
matrix.vec_mul_neg
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[ring α]
(v : m → α)
(A : matrix m n α) :
matrix.vec_mul v (-A) = -matrix.vec_mul v A
@[simp]
theorem
matrix.transpose_one
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α] :
@[instance]
def
matrix.star_ring
{n : Type u_3}
[fintype n]
[decidable_eq n]
{R : Type u_7}
[semiring R]
[star_ring R] :
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 := _}
@[simp]
theorem
matrix.star_apply
{n : Type u_3}
[fintype n]
[decidable_eq n]
{R : Type u_7}
[semiring R]
[star_ring R]
(M : matrix n n R)
(i j : n) :
def
matrix.minor
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix m n α)
(row : l → m)
(col : o → n) :
matrix l o α
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.
theorem
matrix.minor_smul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
{R : Type u_5}
[semiring R]
[add_comm_monoid α]
[semimodule R α]
(r : R)
(A : matrix m n α) :
theorem
matrix.minor_diagonal
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[decidable_eq m]
[decidable_eq l]
(d : m → α)
(e : l → m)
(he : function.injective e) :
(matrix.diagonal d).minor e e = matrix.diagonal (d ∘ e)
If the minor doesn't repeat elements, then when applied to a diagonal matrix the result is diagonal.
theorem
matrix.minor_one
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[has_one α]
[decidable_eq m]
[decidable_eq l]
(e : l → m)
(he : function.injective e) :
theorem
matrix.minor_mul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[semiring α]
{p : Type u_5}
{q : Type u_6}
[fintype p]
[fintype q]
(M : matrix m n α)
(N : matrix n p α)
(e₁ : l → m)
(e₂ : o → n)
(e₃ : q → p)
(he₂ : function.bijective e₂) :
simp lemmas for matrix.minors interaction with matrix.diagonal, 1, and matrix.mul for
when the mappings are bundled.
@[simp]
theorem
matrix.minor_diagonal_embedding
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[decidable_eq m]
[decidable_eq l]
(d : m → α)
(e : l ↪ m) :
(matrix.diagonal d).minor ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
@[simp]
theorem
matrix.minor_diagonal_equiv
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[decidable_eq m]
[decidable_eq l]
(d : m → α)
(e : l ≃ m) :
(matrix.diagonal d).minor ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
@[simp]
theorem
matrix.minor_one_embedding
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[has_one α]
[decidable_eq m]
[decidable_eq l]
(e : l ↪ m) :
@[simp]
theorem
matrix.minor_one_equiv
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[has_zero α]
[has_one α]
[decidable_eq m]
[decidable_eq l]
(e : l ≃ m) :
@[simp]
theorem
matrix.reindex_refl_refl
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
(A : matrix m n α) :
⇑(matrix.reindex (equiv.refl m) (equiv.refl n)) A = A
@[simp]
theorem
matrix.reindex_symm
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(eₘ : m ≃ l)
(eₙ : n ≃ o) :
(matrix.reindex eₘ eₙ).symm = matrix.reindex eₘ.symm eₙ.symm
@[simp]
theorem
matrix.reindex_trans
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
{l₂ : Type u_5}
{o₂ : Type u_6}
[fintype l₂]
[fintype o₂]
(eₘ : m ≃ l)
(eₙ : n ≃ o)
(eₘ₂ : l ≃ l₂)
(eₙ₂ : o ≃ o₂) :
(matrix.reindex eₘ eₙ).trans (matrix.reindex eₘ₂ eₙ₂) = matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)
row_col section #
Simplification lemmas for matrix.row and matrix.col.
@[simp]
theorem
matrix.col_add
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v w : m → α) :
matrix.col (v + w) = matrix.col v + matrix.col w
@[simp]
theorem
matrix.col_smul
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(x : α)
(v : m → α) :
matrix.col (x • v) = x • matrix.col v
@[simp]
theorem
matrix.row_add
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(v w : m → α) :
matrix.row (v + w) = matrix.row v + matrix.row w
@[simp]
theorem
matrix.row_smul
{m : Type u_2}
[fintype m]
{α : Type v}
[semiring α]
(x : α)
(v : m → α) :
matrix.row (x • v) = x • matrix.row v
@[simp]
theorem
matrix.col_apply
{m : Type u_2}
[fintype m]
{α : Type v}
(v : m → α)
(i : m)
(j : unit) :
matrix.col v i j = v i
@[simp]
theorem
matrix.row_apply
{m : Type u_2}
[fintype m]
{α : Type v}
(v : m → α)
(i : unit)
(j : m) :
matrix.row v i j = v j
@[simp]
theorem
matrix.transpose_col
{m : Type u_2}
[fintype m]
{α : Type v}
(v : m → α) :
(matrix.col v)ᵀ = matrix.row v
@[simp]
theorem
matrix.transpose_row
{m : Type u_2}
[fintype m]
{α : Type v}
(v : m → α) :
(matrix.row v)ᵀ = matrix.col v
theorem
matrix.row_vec_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α)
(v : m → α) :
matrix.row (matrix.vec_mul v M) = matrix.row v ⬝ M
theorem
matrix.col_vec_mul
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α)
(v : m → α) :
matrix.col (matrix.vec_mul v M) = (matrix.row v ⬝ M)ᵀ
theorem
matrix.col_mul_vec
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α)
(v : n → α) :
matrix.col (M.mul_vec v) = M ⬝ matrix.col v
theorem
matrix.row_mul_vec
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[semiring α]
(M : matrix m n α)
(v : n → α) :
matrix.row (M.mul_vec v) = (M ⬝ matrix.col v)ᵀ
def
matrix.update_row
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[decidable_eq n]
(M : matrix n m α)
(i : n)
(b : m → α) :
matrix n m α
Update, i.e. replace the ith row of matrix A with the values in b.
Equations
- M.update_row i b = function.update M i b
def
matrix.update_column
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
[decidable_eq m]
(M : matrix n m α)
(j : m)
(b : n → α) :
matrix n m α
Update, i.e. replace the jth column of matrix A with the values in b.
Equations
- M.update_column j b = λ (i : n), function.update (M i) j (b i)
@[simp]
theorem
matrix.update_row_self
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{b : m → α}
[decidable_eq n] :
M.update_row i b i = b
@[simp]
theorem
matrix.update_column_self
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{j : m}
{c : n → α}
[decidable_eq m] :
M.update_column j c i j = c i
@[simp]
theorem
matrix.update_row_ne
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{b : m → α}
[decidable_eq n]
{i' : n}
(i_ne : i' ≠ i) :
M.update_row i b i' = M i'
@[simp]
theorem
matrix.update_column_ne
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{j : m}
{c : n → α}
[decidable_eq m]
{j' : m}
(j_ne : j' ≠ j) :
M.update_column j c i j' = M i j'
theorem
matrix.update_row_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{j : m}
{b : m → α}
[decidable_eq n]
{i' : n} :
M.update_row i b i' j = ite (i' = i) (b j) (M i' j)
theorem
matrix.update_column_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{j : m}
{c : n → α}
[decidable_eq m]
{j' : m} :
M.update_column j c i j' = ite (j' = j) (c i) (M i j')
theorem
matrix.update_row_transpose
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{j : m}
{c : n → α}
[decidable_eq m] :
Mᵀ.update_row j c = (M.update_column j c)ᵀ
theorem
matrix.update_column_transpose
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
{M : matrix n m α}
{i : n}
{b : m → α}
[decidable_eq n] :
Mᵀ.update_column i b = (M.update_row i b)ᵀ
def
matrix.from_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
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))
@[simp]
theorem
matrix.from_blocks_apply₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : n)
(j : l) :
A.from_blocks B C D (sum.inl i) (sum.inl j) = A i j
@[simp]
theorem
matrix.from_blocks_apply₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : n)
(j : m) :
A.from_blocks B C D (sum.inl i) (sum.inr j) = B i j
@[simp]
theorem
matrix.from_blocks_apply₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : o)
(j : l) :
A.from_blocks B C D (sum.inr i) (sum.inl j) = C i j
@[simp]
theorem
matrix.from_blocks_apply₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(i : o)
(j : m) :
A.from_blocks B C D (sum.inr i) (sum.inr j) = D i j
def
matrix.to_blocks₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix n l α
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)
def
matrix.to_blocks₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix n m α
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)
def
matrix.to_blocks₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix o l α
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)
def
matrix.to_blocks₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
matrix o m α
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)
theorem
matrix.from_blocks_to_blocks
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : matrix (n ⊕ o) (l ⊕ m) α) :
M.to_blocks₁₁.from_blocks M.to_blocks₁₂ M.to_blocks₂₁ M.to_blocks₂₂ = M
@[simp]
theorem
matrix.to_blocks_from_blocks₁₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(A.from_blocks B C D).to_blocks₁₁ = A
@[simp]
theorem
matrix.to_blocks_from_blocks₁₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(A.from_blocks B C D).to_blocks₁₂ = B
@[simp]
theorem
matrix.to_blocks_from_blocks₂₁
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(A.from_blocks B C D).to_blocks₂₁ = C
@[simp]
theorem
matrix.to_blocks_from_blocks₂₂
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
(A.from_blocks B C D).to_blocks₂₂ = D
def
matrix.to_block
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
(M : matrix m n α)
(p : m → Prop)
[decidable_pred p]
(q : n → Prop)
[decidable_pred q] :
matrix {a // p a} {a // q a} α
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.
@[simp]
theorem
matrix.to_block_apply
{m : Type u_2}
{n : Type u_3}
[fintype m]
[fintype n]
{α : Type v}
(M : matrix m n α)
(p : m → Prop)
[decidable_pred p]
(q : n → Prop)
[decidable_pred q]
(i : {a // p a})
(j : {a // q a}) :
def
matrix.to_square_block'
{m : Type u_2}
[fintype m]
{α : Type v}
(M : matrix m m α)
(b : m → ℕ)
(k : ℕ) :
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
def
matrix.to_square_block_prop
{m : Type u_2}
[fintype m]
{α : Type v}
(M : matrix m m α)
(p : m → Prop)
[decidable_pred p] :
matrix {a // p a} {a // p a} α
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
@[simp]
theorem
matrix.to_square_block_prop_def
{m : Type u_2}
[fintype m]
{α : Type v}
(M : matrix m m α)
(p : m → Prop)
[decidable_pred p] :
M.to_square_block_prop p = λ (i j : {a // p a}), M ↑i ↑j
theorem
matrix.from_blocks_smul
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[semiring α]
(x : α)
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α) :
x • A.from_blocks B C D = (x • A).from_blocks (x • B) (x • C) (x • D)
theorem
matrix.from_blocks_add
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[semiring α]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(A' : matrix n l α)
(B' : matrix n m α)
(C' : matrix o l α)
(D' : matrix o m α) :
A.from_blocks B C D + A'.from_blocks B' C' D' = (A + A').from_blocks (B + B') (C + C') (D + D')
theorem
matrix.from_blocks_multiply
{l : Type u_1}
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype l]
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[semiring α]
{p : Type u_5}
{q : Type u_6}
[fintype p]
[fintype q]
(A : matrix n l α)
(B : matrix n m α)
(C : matrix o l α)
(D : matrix o m α)
(A' : matrix l p α)
(B' : matrix l q α)
(C' : matrix m p α)
(D' : matrix m q α) :
@[simp]
theorem
matrix.from_blocks_diagonal
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq l]
[decidable_eq m]
(d₁ : l → α)
(d₂ : m → α) :
(matrix.diagonal d₁).from_blocks 0 0 (matrix.diagonal d₂) = matrix.diagonal (sum.elim d₁ d₂)
@[simp]
theorem
matrix.from_blocks_one
{l : Type u_1}
{m : Type u_2}
[fintype l]
[fintype m]
{α : Type v}
[semiring α]
[decidable_eq l]
[decidable_eq m] :
1.from_blocks 0 0 1 = 1
def
matrix.block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
[has_zero α] :
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
@[simp]
theorem
matrix.block_diagonal_apply_eq
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
[has_zero α]
(i : m)
(j : n)
(k : o) :
matrix.block_diagonal M (i, k) (j, k) = M k i j
theorem
matrix.block_diagonal_apply_ne
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
[has_zero α]
(i : m)
(j : n)
{k k' : o}
(h : k ≠ k') :
matrix.block_diagonal M (i, k) (j, k') = 0
@[simp]
theorem
matrix.block_diagonal_transpose
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
[has_zero α] :
(matrix.block_diagonal M)ᵀ = matrix.block_diagonal (λ (k : o), (M k)ᵀ)
@[simp]
theorem
matrix.block_diagonal_zero
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal_diagonal
{m : Type u_2}
{o : Type u_4}
[fintype m]
[fintype o]
{α : Type v}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
(d : o → m → α) :
matrix.block_diagonal (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : m × o), d ik.snd ik.fst)
@[simp]
theorem
matrix.block_diagonal_one
{m : Type u_2}
{o : Type u_4}
[fintype m]
[fintype o]
{α : Type v}
[decidable_eq o]
[has_zero α]
[decidable_eq m]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal_add
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M N : o → matrix m n α)
[decidable_eq o]
[add_monoid α] :
@[simp]
theorem
matrix.block_diagonal_neg
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
[add_group α] :
@[simp]
theorem
matrix.block_diagonal_sub
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M N : o → matrix m n α)
[decidable_eq o]
[add_group α] :
@[simp]
theorem
matrix.block_diagonal_mul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
{p : Type u_1}
[fintype p]
[semiring α]
(N : o → matrix n p α) :
matrix.block_diagonal (λ (k : o), M k ⬝ N k) = matrix.block_diagonal M ⬝ matrix.block_diagonal N
@[simp]
theorem
matrix.block_diagonal_smul
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
(M : o → matrix m n α)
[decidable_eq o]
{R : Type u_1}
[semiring R]
[add_comm_monoid α]
[semimodule R α]
(x : R) :
matrix.block_diagonal (x • M) = x • matrix.block_diagonal M
def
matrix.block_diagonal'
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[has_zero α] :
matrix (Σ (i : o), m' i) (Σ (i : o), n' i) α
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.
theorem
matrix.block_diagonal'_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α)
{k k' : o}
(i : m)
(j : n) :
matrix.block_diagonal M (i, k) (j, k') = matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩
theorem
matrix.block_diagonal'_minor_eq_block_diagonal
{m : Type u_2}
{n : Type u_3}
{o : Type u_4}
[fintype m]
[fintype n]
[fintype o]
{α : Type v}
[decidable_eq o]
[has_zero α]
(M : o → matrix m n α) :
theorem
matrix.block_diagonal'_apply
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[has_zero α]
(ik : Σ (i : o), m' i)
(jk : Σ (i : o), n' i) :
@[simp]
theorem
matrix.block_diagonal'_apply_eq
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[has_zero α]
(k : o)
(i : m' k)
(j : n' k) :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k, j⟩ = M k i j
theorem
matrix.block_diagonal'_apply_ne
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[has_zero α]
{k k' : o}
(i : m' k)
(j : n' k')
(h : k ≠ k') :
matrix.block_diagonal' M ⟨k, i⟩ ⟨k', j⟩ = 0
@[simp]
theorem
matrix.block_diagonal'_transpose
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[has_zero α] :
(matrix.block_diagonal' M)ᵀ = matrix.block_diagonal' (λ (k : o), (M k)ᵀ)
@[simp]
theorem
matrix.block_diagonal'_zero
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
[decidable_eq o]
[has_zero α] :
@[simp]
theorem
matrix.block_diagonal'_diagonal
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{α : Type v}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
(d : Π (i : o), m' i → α) :
matrix.block_diagonal' (λ (k : o), matrix.diagonal (d k)) = matrix.diagonal (λ (ik : Σ (i : o), m' i), d ik.fst ik.snd)
@[simp]
theorem
matrix.block_diagonal'_one
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{α : Type v}
[decidable_eq o]
[has_zero α]
[Π (i : o), decidable_eq (m' i)]
[has_one α] :
@[simp]
theorem
matrix.block_diagonal'_add
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M N : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[add_monoid α] :
@[simp]
theorem
matrix.block_diagonal'_neg
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[add_group α] :
@[simp]
theorem
matrix.block_diagonal'_sub
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M N : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
[add_group α] :
@[simp]
theorem
matrix.block_diagonal'_mul
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
{p : o → Type u_1}
[Π (i : o), fintype (p i)]
[semiring α]
(N : Π (i : o), matrix (n' i) (p i) α) :
matrix.block_diagonal' (λ (k : o), M k ⬝ N k) = matrix.block_diagonal' M ⬝ matrix.block_diagonal' N
@[simp]
theorem
matrix.block_diagonal'_smul
{o : Type u_4}
[fintype o]
{m' : o → Type u_5}
[Π (i : o), fintype (m' i)]
{n' : o → Type u_6}
[Π (i : o), fintype (n' i)]
{α : Type v}
(M : Π (i : o), matrix (m' i) (n' i) α)
[decidable_eq o]
{R : Type u_1}
[semiring R]
[add_comm_monoid α]
[semimodule R α]
(x : R) :
matrix.block_diagonal' (x • M) = x • matrix.block_diagonal' M