Matrices
Equations
- matrix.col w x y = w x
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]
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
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}
(a : i ≠ j) :
1 i j = 0
theorem
matrix.one_apply_ne'
{n : Type u_3}
[fintype n]
{α : Type v}
[decidable_eq n]
[has_zero α]
[has_one α]
{i j : n}
(a : j ≠ i) :
1 i j = 0
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 α
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_6}
@[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 := _}
@[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 := _, 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 := _}
@[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)
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 := _, neg := add_comm_group.neg matrix.add_comm_group, 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 := _}
@[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 (λ (a : 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 α
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 → α)
(a : m) :
α
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 α)
(a : n) :
α
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 α] :
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 ith 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 correspnding "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 correspnding "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 correspnding "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 correspnding "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
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 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
@[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