# mathlibdocumentation

data.matrix.basic

# Matrices #

@[nolint]
def matrix (m : Type u) (n : Type u') [fintype m] [fintype n] (α : Type v) :
Type (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
• n α = (m → n → α)
theorem matrix.ext_iff {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {M N : 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 : 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 : n α) {β : Type w} (f : α → β) :
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 : n α} {β : Type w} {f : α → β} {i : m} {j : n} :
M.map f i j = f (M i j)
@[simp]
theorem matrix.map_map {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} {M : n α} {β : Type u_1} {γ : Type u_4} {f : α → β} {g : β → γ} :
(M.map f).map g = M.map (g f)
def matrix.transpose {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : n α) :
m α

The transpose of a matrix.

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

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

Equations
• x y = w x
def matrix.row {n : Type u_3} [fintype n] {α : Type v} (v : n → α) :
α

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

Equations
• x y = v y
@[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 α] :
Equations
@[instance]
def matrix.add_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v}  :
Equations
@[instance]
def matrix.add_comm_semigroup {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v}  :
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}  :
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.has_sub {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_sub α] :
has_sub (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 α] :
Equations
@[instance]
def matrix.add_comm_group {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v}  :
Equations
@[instance]
def matrix.unique {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [unique α] :
unique (matrix m n α)
Equations
@[instance]
def matrix.subsingleton {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [subsingleton α] :
@[instance]
def matrix.nontrivial {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [nonempty m] [nonempty n] [nontrivial α] :
@[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 : 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 : n α) (i : m) (j : n) :
(M + N) i j = M i j + N i j
@[simp]
theorem matrix.sub_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [has_sub α] (M N : 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 : α → β} (h : f 0 = 0) :
0.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 : 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 : 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} (hm : ¬) :
theorem matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (hn : ¬) :
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 : α →+ β) :
n α →+ 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 : n α) :
def matrix.diagonal {n : Type u_3} [fintype n] {α : Type v} [decidable_eq n] [has_zero α] (d : 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
• = λ (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) :
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) :
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) :
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 (λ (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 → α} :
.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 : α → β} (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
1.map f = 1
@[simp]
theorem matrix.bit0_apply {m : Type u_2} [fintype m] {α : Type v} [has_add α] (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 : 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 : 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 : n α) {i j : n} (h : i j) :
bit1 M i j = bit0 (M i j)
def matrix.dot_product {m : Type u_2} [fintype m] {α : Type v} [has_mul α] (v w : m → α) :
α

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

Equations
• = ∑ (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), (λ (i : m), v i j)) w = (λ (i : m), matrix.dot_product (v i) w)
theorem matrix.dot_product_comm {m : Type u_2} [fintype m] {α : Type v} (v w : m → α) :
@[simp]
theorem matrix.dot_product_punit {α : Type v} [has_mul α] (v w : punit → α) :
= (v punit.star) *
@[simp]
theorem matrix.dot_product_zero {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v : m → α) :
= 0
@[simp]
theorem matrix.dot_product_zero' {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v : m → α) :
(λ (_x : m), 0) = 0
@[simp]
theorem matrix.zero_dot_product {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v : m → α) :
= 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 → α) :
@[simp]
theorem matrix.dot_product_add {m : Type u_2} [fintype m] {α : Type v} [semiring α] (u v w : m → α) :
(v + w) =
@[simp]
theorem matrix.diagonal_dot_product {m : Type u_2} [fintype m] {α : Type v} [decidable_eq m] [semiring α] (v w : m → α) (i : m) :
= (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) :
= (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) :
(λ (j : m), i) = (v i) * w i
@[simp]
theorem matrix.neg_dot_product {m : Type u_2} [fintype m] {α : Type v} [ring α] (v w : m → α) :
w =
@[simp]
theorem matrix.dot_product_neg {m : Type u_2} [fintype m] {α : Type v} [ring α] (v w : m → α) :
(-w) =
@[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} (x : α) (v w : m → α) :
(x w) = x *
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 α] (M : m α) (N : n α) :
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 α] {M : m α} {N : 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 α]  :
has_mul (matrix n n α)
Equations
@[simp]
theorem matrix.mul_eq_mul {n : Type u_3} [fintype n] {α : Type v} [has_mul α] (M N : n α) :
M * N = M N
theorem matrix.mul_apply' {n : Type u_3} [fintype n] {α : Type v} [has_mul α] {M 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 : m α) (M : n α) (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 (λ (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 : 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 : 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 : n α) (M 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 : m α) (N : 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 : n α) (i : m) (j : n) :
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 : n α) (i : m) (j : n) :
(M 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 : 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 : 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
@[instance]
def matrix.semiring {n : Type u_3} [fintype n] {α : Type v} [semiring α] [decidable_eq n] :
semiring (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 (λ (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 (λ (i : n), (d₁ i) * d₂ i)
@[simp]
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 : n α} {M : o α} {β : Type w} [semiring β] {f : α →+* β} :
(L M).map f = L.map f M.map f
@[simp]
theorem matrix.ring_hom_map_one {n : Type u_3} [fintype n] {α : Type v} [semiring α] [decidable_eq n] {β : Type w} [semiring β] (f : α →+* β) :
1.map f = 1

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 : α ≃+* β) :
1.map f = 1

A version of `one_map` where `f` is a `ring_equiv`.

@[simp]
theorem matrix.zero_hom_map_zero {n : Type u_3} [fintype n] {α : Type v} [semiring α] {β : Type w} [has_zero β] (f : β) :
0.map f = 0

A version of `map_zero` where `f` is a `zero_hom`.

@[simp]
theorem matrix.add_monoid_hom_map_zero {n : Type u_3} [fintype n] {α : Type v} [semiring α] {β : Type w} [add_monoid β] (f : α →+ β) :
0.map f = 0

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 : α ≃+ β) :
0.map f = 0

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} [ α] [ β] (f : α →ₗ[R] β) :
0.map f = 0

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} [ α] [ β] (f : α ≃ₗ[R] β) :
0.map f = 0

A version of `map_zero` where `f` is a `linear_equiv`.

@[simp]
theorem matrix.ring_hom_map_zero {n : Type u_3} [fintype n] {α : Type v} [semiring α] {β : Type w} [semiring β] (f : α →+* β) :
0.map f = 0

A version of `map_zero` where `f` is a `ring_hom`.

@[simp]
theorem matrix.ring_equiv_map_zero {n : Type u_3} [fintype n] {α : Type v} [semiring α] {β : Type w} [semiring β] (f : α ≃+* β) :
0.map f = 0

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 : m α) :
is_add_monoid_hom (λ (x : 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 : n α) :
is_add_monoid_hom (λ (x : 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 : β → m α) (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 : β → n α) (M : 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) :
i j =
def ring_hom.map_matrix {m : Type u_2} [fintype m] {α : Type v} [decidable_eq m] [semiring α] {β : Type w} [semiring β] (f : α →+* β) :
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 : 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 : n α) (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 : n α) (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' : n α) (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 : n α) (N N' : o α) :
M (N - N') = M N - M N'
@[instance]
def matrix.ring {n : Type u_3} [fintype n] {α : Type v} [decidable_eq n] [ring α] :
ring (matrix n n α)
Equations
@[instance]
def matrix.has_scalar {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] :
(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 α] [ β] :
(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 : 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 : 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 : n α) (a : α) (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 : n α) (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] :
α →+* 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] :
= λ (a : α), a 1
theorem matrix.scalar_apply_eq {n : Type u_3} [fintype n] {α : Type v} [semiring α] [decidable_eq n] (a : α) (i : 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) :
a i j = 0
theorem matrix.scalar_inj {n : Type u_3} [fintype n] {α : Type v} [semiring α] [decidable_eq n] [nonempty n] {r s : α} :
r = s r = s
theorem matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [decidable_eq n] (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} (M : n α) (a : α) (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} (M : n α) (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} [decidable_eq n] (r : α) (M : n α) :
commute ( 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 → α) :
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
• 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 : 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
def matrix.vec_mul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (v : m → α) (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
• j = (λ (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 : 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) :
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) :
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 → α) :
= v
@[simp]
theorem matrix.mul_vec_zero {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (A : 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 : n α) :
= 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 : n α) (N : o α) :
N = (M N)
@[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 : n α) (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] (i : m) (j : n) (a : α) :
n α

`std_basis_matrix i j a` is the matrix with `a` in the `i`-th row, `j`-th column, and zeroes elsewhere.

Equations
• = λ (i' : m) (j' : n), ite (i' = i j' = j) a 0
@[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 = (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) :
= 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 : α) :
(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 : m α) :
x = ∑ (i : n) (j : m), (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.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 : n X → Prop} (m : n X) (h_zero : M 0) (h_add : ∀ (p q : n X), M pM qM (p + q)) (h_std_basis : ∀ (i j : n) (x : X), M 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 : n X → Prop} (m : n X) (h_add : ∀ (p q : n X), M pM qM (p + q)) (h_std_basis : ∀ (i j : n) (x : X), M 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 : n α) :
A = -
theorem matrix.vec_mul_neg {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [ring α] (v : m → α) (A : n α) :
(-A) = -
theorem matrix.neg_mul_vec {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [ring α] (v : n → α) (A : 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 : 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 : 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 : 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 : 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 : 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 : 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} (M : n α) (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 : 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 : 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 : n α} :
M.map f = (M.map f)
@[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
@[simp]
theorem matrix.star_apply {n : Type u_3} [fintype n] [decidable_eq n] {R : Type u_7} [semiring R] [star_ring R] (M : n R) (i j : n) :
star M i j = star (M j i)
theorem matrix.star_mul {n : Type u_3} [fintype n] [decidable_eq n] {R : Type u_7} [semiring R] [star_ring R] (M N : n R) :
star (M N) = star N star M
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 : n α) (row : l → m) (col : o → n) :
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)
@[simp]
theorem matrix.minor_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 : n α) (row : l → m) (col : o → n) (i : l) (j : o) :
A.minor row col i j = A (row i) (col j)
@[simp]
theorem matrix.minor_id_id {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (A : n α) :
A.minor id id = A
@[simp]
theorem matrix.minor_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} {l₂ : Type u_5} {o₂ : Type u_6} [fintype l₂] [fintype o₂] (A : n α) (row₁ : l → m) (col₁ : o → n) (row₂ : l₂ → l) (col₂ : o₂ → o) :
(A.minor row₁ col₁).minor row₂ col₂ = A.minor (row₁ row₂) (col₁ col₂)
@[simp]
theorem matrix.transpose_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 : n α) (row : l → m) (col : o → n) :
(A.minor row col) = A.minor col row
theorem matrix.minor_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} [has_add α] (A B : n α) :
(A + B).minor = A.minor + B.minor
theorem matrix.minor_neg {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} [has_neg α] (A : n α) :
theorem matrix.minor_sub {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} [has_sub α] (A B : n α) :
(A - B).minor = A.minor - B.minor
@[simp]
theorem matrix.minor_zero {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} [has_zero α] :
0.minor = 0
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] [ α] (r : R) (A : n α) :
(r A).minor = r A.minor
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) :

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) :
1.minor e e = 1
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 : n α) (N : p α) (e₁ : l → m) (e₂ : o → n) (e₃ : q → p) (he₂ : function.bijective e₂) :
(M N).minor e₁ e₃ = M.minor e₁ e₂ N.minor e₂ e₃

`simp` lemmas for `matrix.minor`s 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) :
@[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) :
@[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) :
1.minor e e = 1
@[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) :
1.minor e e = 1
theorem matrix.minor_mul_equiv {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 : n α) (N : p α) (e₁ : l → m) (e₂ : o n) (e₃ : q → p) :
(M N).minor e₁ e₃ = M.minor e₁ e₂ N.minor e₂ e₃
def matrix.reindex {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) :
n α o α

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations
@[simp]
theorem matrix.reindex_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} (eₘ : m l) (eₙ : n o) (M : n α) :
eₙ) M = M.minor (eₘ.symm) (eₙ.symm)
@[simp]
theorem matrix.reindex_refl_refl {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (A : n α) :
(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) :
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₂) :
eₙ).trans (matrix.reindex eₘ₂ eₙ₂) = matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)
theorem matrix.transpose_reindex {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) (M : n α) :
( eₙ) M) = eₘ) M
def matrix.sub_left {α : Type v} {m l r : } (A : 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 : } (A : 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 : } (A : 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 : } (A : 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 : } (A : 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 : } (A : 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 : } (A : 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 : } (A : 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 → α) :
matrix.col (v + w) =
@[simp]
theorem matrix.col_smul {m : Type u_2} [fintype m] {α : Type v} [semiring α] (x : α) (v : m → α) :
matrix.col (x v) = x
@[simp]
theorem matrix.row_add {m : Type u_2} [fintype m] {α : Type v} [semiring α] (v w : m → α) :
matrix.row (v + w) =
@[simp]
theorem matrix.row_smul {m : Type u_2} [fintype m] {α : Type v} [semiring α] (x : α) (v : m → α) :
matrix.row (x v) = x
@[simp]
theorem matrix.col_apply {m : Type u_2} [fintype m] {α : Type v} (v : m → α) (i : m) (j : unit) :
i j = v i
@[simp]
theorem matrix.row_apply {m : Type u_2} [fintype m] {α : Type v} (v : m → α) (i : unit) (j : m) :
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 : n α) (v : m → α) :
theorem matrix.col_vec_mul {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (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 : n α) (v : n → α) :
theorem matrix.row_mul_vec {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} [semiring α] (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] (M : m α) (i : n) (b : m → α) :
m α

Update, i.e. replace the `i`th 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] (M : m α) (j : m) (b : n → α) :
m α

Update, i.e. replace the `j`th 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 : 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 : m α} {i : n} {j : m} {c : n → α} [decidable_eq m] :
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 : 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 : m α} {i : n} {j : m} {c : n → α} [decidable_eq m] {j' : m} (j_ne : j' 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 : 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 : m α} {i : n} {j : m} {c : n → α} [decidable_eq m] {j' : m} :
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 : 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 : m α} {i : n} {b : m → α} [decidable_eq n] :
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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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) α) :
l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "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} (M : matrix (n o) (l m) α) :
m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "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} (M : matrix (n o) (l m) α) :
l α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "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} (M : matrix (n o) (l m) α) :
m α

Given a matrix whose row and column indexes are sum types, we can extract the corresponding "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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : m α) :
(A.from_blocks B C D) = B D
def matrix.to_block {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : n α) (p : m → Prop) (q : n → Prop)  :
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.

Equations
@[simp]
theorem matrix.to_block_apply {m : Type u_2} {n : Type u_3} [fintype m] [fintype n] {α : Type v} (M : n α) (p : m → Prop) (q : n → Prop) (i : {a // p a}) (j : {a // q a}) :
M.to_block p q i j = M i j
def matrix.to_square_block {m : Type u_2} [fintype m] {α : Type v} (M : m α) {n : } (b : m → fin n) (k : fin n) :
matrix {a // b a = k} {a // b a = k} α

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
@[simp]
theorem matrix.to_square_block_def {m : Type u_2} [fintype m] {α : Type v} (M : m α) {n : } (b : m → fin n) (k : fin n) :
k = λ (i j : {a // b a = k}), M i j
def matrix.to_square_block' {m : Type u_2} [fintype m] {α : Type v} (M : m α) (b : m → ) (k : ) :
matrix {a // b a = k} {a // b a = 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
@[simp]
theorem matrix.to_square_block_def' {m : Type u_2} [fintype m] {α : Type v} (M : m α) (b : m → ) (k : ) :
k = λ (i j : {a // b a = k}), M i j
def matrix.to_square_block_prop {m : Type u_2} [fintype m] {α : Type v} (M : m α) (p : m → Prop)  :
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
@[simp]
theorem matrix.to_square_block_prop_def {m : Type u_2} [fintype m] {α : Type v} (M : m α) (p : m → Prop)  :
= λ (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 : l α) (B : m α) (C : l α) (D : 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 : l α) (B : m α) (C : l α) (D : m α) (A' : l α) (B' : m α) (C' : l α) (D' : 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 : l α) (B : m α) (C : l α) (D : m α) (A' : p α) (B' : q α) (C' : p α) (D' : 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 → α) :
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 → n α) [decidable_eq o] [has_zero α] :
matrix (m × o) (n × o) α

`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
• (i, k) (j, k') = ite (k = k') (M k i j) 0
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 → n α) [decidable_eq o] [has_zero α] (ik : m × o) (jk : n × o) :
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 → n α) [decidable_eq o] [has_zero α] (i : m) (j : n) (k : o) :
(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 → n α) [decidable_eq o] [has_zero α] (i : m) (j : n) {k k' : o} (h : k k') :
(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 → n α) [decidable_eq o] [has_zero α] :
= 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 → 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 → 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 → 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 → n α) [decidable_eq o] {p : Type u_1} [fintype p] [semiring α] (N : o → p α) :
matrix.block_diagonal (λ (k : o), M k N k) =
@[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 → n α) [decidable_eq o] {R : Type u_1} [semiring R] [ α] (x : R) :
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`.

Equations
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 → n α) {k k' : o} (i : m) (j : n) :
(i, k) (j, k') = 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 → 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) :
jk = dite (ik.fst = jk.fst) (λ (h : ik.fst = jk.fst), M ik.fst ik.snd (cast _ jk.snd)) (λ (h : ¬ik.fst = jk.fst), 0)
@[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) :
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') :
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' (λ (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) =
@[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] [ α] (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_7} [semiring α] [semiring β] (M : n α) (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