mathlib documentation

data.matrix.basic

Matrices

@[nolint]
def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] :
Type vType (max u u' v)

matrix m n is the type of matrices whose rows are indexed by the fintype m and whose columns are indexed by the fintype n.

Equations
theorem matrix.ext_iff {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {M N : matrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) M = N

@[ext]
theorem matrix.ext {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {M N : matrix m n α} :
(∀ (i : m) (j : n), M i j = N i j)M = N

def matrix.map {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : matrix m n α) {β : Type w} :
(α → β)matrix m n β

M.map f is the matrix obtained by applying f to each entry of the matrix M.

Equations
  • M.map f = λ (i : m) (j : n), f (M i j)
@[simp]
theorem matrix.map_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {M : matrix m n α} {β : Type w} {f : α → β} {i : m} {j : n} :
M.map f i j = f (M i j)

def matrix.transpose {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} :
matrix m n αmatrix n m α

The transpose of a matrix.

Equations
def matrix.col {m : Type u_2} [fintype m] {α : Type v} :
(m → α)matrix m unit α

matrix.col u is the column matrix whose entries are given by u.

Equations
def matrix.row {n : Type u_3} [fintype n] {α : Type v} :
(n → α)matrix unit n α

matrix.row u is the row matrix whose entries are given by u.

Equations
@[instance]
def matrix.inhabited {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [inhabited α] :
inhabited (matrix m n α)

Equations
@[instance]
def matrix.has_add {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_add α] :
has_add (matrix m n α)

Equations
@[instance]
def matrix.add_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_semigroup α] :

Equations
@[instance]
def matrix.add_comm_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_comm_semigroup α] :

Equations
@[instance]
def matrix.has_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_zero α] :
has_zero (matrix m n α)

Equations
@[instance]
def matrix.add_monoid {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_monoid α] :

Equations
@[instance]
def matrix.add_comm_monoid {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_comm_monoid α] :

Equations
@[instance]
def matrix.has_neg {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_neg α] :
has_neg (matrix m n α)

Equations
@[instance]
def matrix.add_group {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_group α] :
add_group (matrix m n α)

Equations
@[instance]
def matrix.add_comm_group {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_comm_group α] :

Equations
@[simp]
theorem matrix.zero_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_zero α] (i : m) (j : n) :
0 i j = 0

@[simp]
theorem matrix.neg_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_neg α] (M : matrix m n α) (i : m) (j : n) :
(-M) i j = -M i j

@[simp]
theorem matrix.add_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_add α] (M N : matrix m n α) (i : m) (j : n) :
(M + N) i j = M i j + N i j

@[simp]
theorem matrix.map_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_zero α] {β : Type w} [has_zero β] {f : α → β} :
f 0 = 00.map f = 0

theorem matrix.map_add {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_monoid α] {β : Type w} [add_monoid β] (f : α →+ β) (M N : matrix m n α) :
(M + N).map f = M.map f + N.map f

theorem matrix.map_sub {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_group α] {β : Type w} [add_group β] (f : α →+ β) (M N : matrix m n α) :
(M - N).map f = M.map f - N.map f

theorem matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} :

theorem matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} :

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 β] :
→+ β)matrix m n α →+ matrix m n β

The add_monoid_hom between spaces of matrices induced by an add_monoid_hom between their coefficients.

Equations
@[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 α) :

def matrix.diagonal {n : Type u_3} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] :
(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
@[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} :
i jmatrix.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} :
j imatrix.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 → α) :

@[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 α] :
has_one (matrix n n α)

Equations
@[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} :
1 i j = ite (i = j) 1 0

@[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} :
i j1 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} :
j i1 i j = 0

@[simp]
theorem matrix.one_map {n : Type u_3} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {β : Type w} [has_zero β] [has_one β] {f : α → β} :
f 0 = 0f 1 = 11.map f = 1

@[simp]
theorem matrix.bit0_apply {m : Type u_2} [fintype m] {α : Type v} [has_add α] (M : matrix m m α) (i j : m) :
bit0 M i j = bit0 (M i j)

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) :
bit1 M i j = ite (i = j) (bit1 (M i j)) (bit0 (M i j))

@[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) :
bit1 M i i = bit1 (M i i)

@[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} :
i jbit1 M i j = bit0 (M i j)

def matrix.dot_product {m : Type u_2} [fintype m] {α : Type v} [has_mul α] [add_comm_monoid α] :
(m → α)(m → α) → α

dot_product v w is the sum of the entrywise products v i * w i

Equations
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 → α) :

@[simp]
theorem matrix.dot_product_punit {α : Type v} [add_comm_monoid α] [has_mul α] (v w : punit → α) :

@[simp]
theorem matrix.dot_product_zero {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v : m → α) :

@[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 → α) :

@[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 → α) :

@[simp]
theorem matrix.dot_product_add {m : Type u_2} [fintype m] {α : Type v} [semiring α] (u v w : m → α) :

@[simp]
theorem matrix.diagonal_dot_product {m : Type u_2} [fintype m] {α : Type v} [decidable_eq m] [semiring α] (v w : m → α) (i : m) :

@[simp]
theorem matrix.dot_product_diagonal {m : Type u_2} [fintype m] {α : Type v} [decidable_eq m] [semiring α] (v w : m → α) (i : m) :

@[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 → α) :

@[simp]
theorem matrix.dot_product_neg {m : Type u_2} [fintype m] {α : Type v} [ring α] (v w : m → α) :

@[simp]
theorem matrix.smul_dot_product {m : Type u_2} [fintype m] {α : Type v} [semiring α] (x : α) (v w : m → α) :

@[simp]
theorem matrix.dot_product_smul {m : Type u_2} [fintype m] {α : Type v} [comm_semiring α] (x : α) (v w : m → α) :

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 α] :
matrix l m α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
theorem matrix.mul_apply {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 α} {i : l} {k : n} :
(M N) i k = ∑ (j : m), (M i j) * N j k

@[instance]
def matrix.has_mul {n : Type u_3} [fintype n] {α : Type v} [has_mul α] [add_comm_monoid α] :
has_mul (matrix n n α)

Equations
@[simp]
theorem matrix.mul_eq_mul {n : Type u_3} [fintype n] {α : Type v} [has_mul α] [add_comm_monoid α] (M N : matrix n n α) :
M * N = M 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)

theorem matrix.mul_assoc {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 α] (L : matrix l m α) (M : matrix m n α) (N : matrix n o α) :
L M N = L (M N)

@[instance]
def matrix.semigroup {n : Type u_3} [fintype n] {α : Type v} [semiring α] :
semigroup (matrix n n α)

Equations
@[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.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [semiring α] (M : matrix m n α) :
M 0 = 0

@[simp]
theorem matrix.zero_mul {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 α) :
0 M = 0

theorem matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [semiring α] (L : matrix m n α) (M N : matrix n o α) :
L (M + N) = L M + L N

theorem matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} [fintype l] [fintype m] [fintype n] {α : Type v} [semiring α] (L M : matrix l m α) (N : matrix m n α) :
(L + M) N = L N + M N

@[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 α) :
1 M = M

@[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 α) :
M 1 = M

@[instance]
def matrix.monoid {n : Type u_3} [fintype n] {α : Type v} [semiring α] [decidable_eq n] :
monoid (matrix n n α)

Equations
@[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.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [semiring α] {L : matrix m n α} {M : matrix n o α} {β : Type w} [semiring β] {f : α →+* β} :
(L M).map f = L.map f M.map f

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)

theorem matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} [fintype l] [fintype m] [fintype n] {α : Type v} [semiring α] {β : Type u_4} (s : finset β) (f : β → matrix l m α) (M : matrix m n α) :
(∑ (a : β) in s, f a) M = ∑ (a : β) in s, f a M

theorem matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} [fintype l] [fintype m] [fintype n] {α : Type v} [semiring α] {β : Type u_4} (s : finset β) (f : β → matrix m n α) (M : matrix l m α) :
M ∑ (a : β) in s, f a = ∑ (a : β) in s, M f a

@[simp]
theorem matrix.row_mul_col_apply {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v w : m → α) (i j : unit) :

def ring_hom.map_matrix {m : Type u_2} [fintype m] {α : Type v} [decidable_eq m] [semiring α] {β : Type w} [semiring β] :
→+* β)matrix m m α →+* matrix m m β

The ring_hom between spaces of square matrices induced by a ring_hom between their coefficients.

Equations
@[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 α) :

@[simp]
theorem matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [ring α] (M : matrix m n α) (N : matrix n o α) :
-M N = -(M N)

@[simp]
theorem matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [ring α] (M : matrix m n α) (N : matrix n o α) :
M -N = -(M N)

theorem matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [ring α] (M M' : matrix m n α) (N : matrix n o α) :
(M - M') N = M N - M' N

theorem matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [ring α] (M : matrix m n α) (N N' : matrix n o α) :
M (N - N') = M N - M N'

@[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
@[simp]
theorem matrix.smul_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) :
(a A) i j = a * A i j

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

@[simp]
theorem matrix.smul_mul {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 α) (a : α) (N : matrix n l α) :
(a M) N = a M N

@[simp]
theorem matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [semiring α] (M : matrix m n α) (N : matrix n o α) (a : α) :
(λ (i : m) (j : n), a * M i j) N = a M N

def matrix.scalar {α : Type v} [semiring α] (n : Type u) [decidable_eq n] [fintype n] :
α →+* matrix n n α

The ring homomorphism α →+* matrix n n α sending a to the diagonal matrix with a on the diagonal.

Equations
@[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) :
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 : α} :

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)

@[simp]
theorem matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} [fintype l] [fintype m] [fintype n] {α : Type v} [comm_semiring α] (M : matrix m n α) (a : α) (N : matrix n l α) :
M (a N) = a M N

@[simp]
theorem matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [comm_semiring α] (M : matrix m n α) (N : matrix n o α) (a : α) :
(M λ (i : n) (j : o), a * N i j) = a M N

theorem matrix.scalar.commute {n : Type u_3} [fintype n] {α : Type v} [comm_semiring α] [decidable_eq n] (r : α) (M : matrix n n α) :

def matrix.vec_mul_vec {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] :
(m → α)(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
def matrix.mul_vec {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] :
matrix m n α(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
def matrix.vec_mul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] :
(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
@[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 → α) :
1.mul_vec v = v

@[simp]
theorem matrix.vec_mul_one {m : Type u_2} [fintype m] {α : Type v} [semiring α] [decidable_eq m] (v : m → α) :

@[simp]
theorem matrix.mul_vec_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (A : matrix m n α) :
A.mul_vec 0 = 0

@[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 α) :

@[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 α) :

@[simp]
theorem matrix.mul_vec_mul_vec {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} [semiring α] (v : o → α) (M : matrix m n α) (N : matrix n o α) :
M.mul_vec (N.mul_vec v) = (M N).mul_vec v

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 → α) :

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] :
m → n → α → 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.

Equations
@[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 : α) :

@[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) :

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 : α) :

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) :
M 0(∀ (p q : matrix n n X), M pM qM (p + q))(∀ (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) :
(∀ (p q : matrix n n X), M pM qM (p + q))(∀ (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 α) :

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 α) :

theorem matrix.neg_mul_vec {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [ring α] (v : n → α) (A : matrix m n α) :
(-A).mul_vec v = -A.mul_vec v

theorem matrix.mul_vec_neg {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [ring α] (v : n → α) (A : matrix m n α) :
A.mul_vec (-v) = -A.mul_vec v

theorem matrix.smul_mul_vec_assoc {n : Type u_3} [fintype n] {α : Type v} [ring α] (A : matrix n n α) (b : n → α) (a : α) :
(a A).mul_vec b = a A.mul_vec b

@[simp]
theorem matrix.transpose_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : matrix m n α) (i : m) (j : n) :
M j i = M i j

Tell simp what the entries are in a transposed matrix.

Compare with mul_apply, diagonal_apply_eq, etc.

@[simp]
theorem matrix.transpose_transpose {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : matrix m n α) :

@[simp]
theorem matrix.transpose_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_zero α] :
0 = 0

@[simp]
theorem matrix.transpose_one {n : Type u_3} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
1 = 1

@[simp]
theorem matrix.transpose_add {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_add α] (M N : matrix m n α) :
(M + N) = M + N

@[simp]
theorem matrix.transpose_sub {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [add_group α] (M N : matrix m n α) :
(M - N) = M - N

@[simp]
theorem matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} [fintype l] [fintype m] [fintype n] {α : Type v} [comm_semiring α] (M : matrix m n α) (N : matrix n l α) :
(M N) = N M

@[simp]
theorem matrix.transpose_smul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (c : α) (M : matrix m n α) :
(c M) = c M

@[simp]
theorem matrix.transpose_neg {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_neg α] (M : matrix m n α) :
(-M) = -M

theorem matrix.transpose_map {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {β : Type w} {f : α → β} {M : matrix m n α} :
M.map f = (M.map f)

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} :
matrix m n α(l → m)(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.

Equations
  • A.minor row col = λ (i : l) (j : o), A (row i) (col j)
def matrix.sub_left {α : Type v} {m l r : } :
matrix (fin m) (fin (l + r)) αmatrix (fin m) (fin l) α

The left n × l part of a n × (l+r) matrix.

Equations
def matrix.sub_right {α : Type v} {m l r : } :
matrix (fin m) (fin (l + r)) αmatrix (fin m) (fin r) α

The right n × r part of a n × (l+r) matrix.

Equations
def matrix.sub_up {α : Type v} {d u n : } :
matrix (fin (u + d)) (fin n) αmatrix (fin u) (fin n) α

The top u × n part of a (u+d) × n matrix.

Equations
def matrix.sub_down {α : Type v} {d u n : } :
matrix (fin (u + d)) (fin n) αmatrix (fin d) (fin n) α

The bottom d × n part of a (u+d) × n matrix.

Equations
def matrix.sub_up_right {α : Type v} {d u l r : } :
matrix (fin (u + d)) (fin (l + r)) αmatrix (fin u) (fin r) α

The top-right u × r part of a (u+d) × (l+r) matrix.

Equations
def matrix.sub_down_right {α : Type v} {d u l r : } :
matrix (fin (u + d)) (fin (l + r)) αmatrix (fin d) (fin r) α

The bottom-right d × r part of a (u+d) × (l+r) matrix.

Equations
def matrix.sub_up_left {α : Type v} {d u l r : } :
matrix (fin (u + d)) (fin (l + r)) αmatrix (fin u) (fin l) α

The top-left u × l part of a (u+d) × (l+r) matrix.

Equations
def matrix.sub_down_left {α : Type v} {d u l r : } :
matrix (fin (u + d)) (fin (l + r)) αmatrix (fin d) (fin l) α

The bottom-left d × l part of a (u+d) × (l+r) matrix.

Equations

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 → α) :

@[simp]
theorem matrix.col_smul {m : Type u_2} [fintype m] {α : Type v} [semiring α] (x : α) (v : m → α) :

@[simp]
theorem matrix.row_add {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v w : m → α) :

@[simp]
theorem matrix.row_smul {m : Type u_2} [fintype m] {α : Type v} [semiring α] (x : α) (v : m → α) :

@[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 → α) :

@[simp]
theorem matrix.transpose_row {m : Type u_2} [fintype m] {α : Type v} (v : m → α) :

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 → α) :

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 → α) :

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 → α) :

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 → α) :

def matrix.update_row {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [decidable_eq n] :
matrix n m αn → (m → α)matrix n m α

Update, i.e. replace the ith row of matrix A with the values in b.

Equations
def matrix.update_column {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [decidable_eq m] :
matrix n m αm → (n → α)matrix n m α

Update, i.e. replace the jth column of matrix A with the values in b.

Equations
@[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' iM.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' jM.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] :

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] :

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} :
matrix n l αmatrix n m αmatrix o l αmatrix o m αmatrix (n o) (l m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Equations
@[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} :
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
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} :
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
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} :
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
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} :
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
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) α) :

@[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 α) :

@[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 α) :

@[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 α) :

@[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 α) :

theorem matrix.from_blocks_transpose {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 α) :

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 α) :
A.from_blocks B C D A'.from_blocks B' C' D' = (A A' + B C').from_blocks (A B' + B D') (C A' + D C') (C B' + D D')

@[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 → α) :

@[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 (m × o) (n × o) α

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
theorem matrix.block_diagonal_apply {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 α] (ik : m × o) (jk : n × o) :
matrix.block_diagonal M ik jk = ite (ik.snd = jk.snd) (M ik.snd ik.fst jk.fst) 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} :
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 α] :

@[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 α) :

@[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) :

theorem ring_hom.map_matrix_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} [fintype m] [fintype n] [fintype o] {α : Type v} {β : Type u_5} [semiring α] [semiring β] (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f : α →+* β) :
f ((M N) i j) = ((λ (i : m) (j : n), f (M i j)) λ (i : n) (j : o), f (N i j)) i j