mathlib documentation

data.matrix.basic

Matrices #

This file defines basic properties of matrices.

Notation #

The locale matrix gives the following notation:

TODO #

Under various conditions, multiplication of infinite matrices makes sense. These have not yet been implemented.

source
def matrix (m : Type u) (n : Type u') (α : Type v) :
Type (max u u' v)

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

Equations
source
theorem matrix.ext_iff {m : Type u_2} {n : Type u_3} {α : Type v} {M N : matrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) ↔ M = N
source
@[ext]
theorem matrix.ext {m : Type u_2} {n : Type u_3} {α : Type v} {M N : matrix m n α} :
(∀ (i : m) (j : n), M i j = N i j) → M = N
source
def matrix.map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : matrix m n α) (f : α → β) :
matrix m n β

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

This is available in bundled forms as:

Equations
  • M.map f = λ (i : m) (j : n), f (M i j)
source
@[simp]
theorem matrix.map_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : matrix m n α} {f : α → β} {i : m} {j : n} :
M.map f i j = f (M i j)
source
@[simp]
theorem matrix.map_id {m : Type u_2} {n : Type u_3} {α : Type v} (M : matrix m n α) :
M.map id = M
source
@[simp]
theorem matrix.map_map {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix m n α} {β : Type u_1} {γ : Type u_4} {f : α → β} {g : β → γ} :
(M.map f).map g = M.map (g ∘ f)
source
def matrix.transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : matrix m n α) :
matrix n m α

The transpose of a matrix.

Equations
source
def matrix.conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [has_star α] (M : matrix m n α) :
matrix n m α

The conjugate transpose of a matrix defined in term of star.

Equations
source
def matrix.col {m : Type u_2} {α : Type v} (w : m → α) :
matrix m unit α

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

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

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

Equations
source
@[protected, instance]
def matrix.inhabited {m : Type u_2} {n : Type u_3} {α : Type v} [inhabited α] :
inhabited (matrix m n α)
Equations
source
@[protected, instance]
def matrix.has_add {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
has_add (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_semigroup {m : Type u_2} {n : Type u_3} {α : Type v} [add_semigroup α] :
add_semigroup (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_comm_semigroup {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_semigroup α] :
add_comm_semigroup (matrix m n α)
Equations
source
@[protected, instance]
def matrix.has_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
has_zero (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_zero_class {m : Type u_2} {n : Type u_3} {α : Type v} [add_zero_class α] :
add_zero_class (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_monoid {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] :
add_monoid (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_comm_monoid {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] :
add_comm_monoid (matrix m n α)
Equations
source
@[protected, instance]
def matrix.has_neg {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] :
has_neg (matrix m n α)
Equations
source
@[protected, instance]
def matrix.has_sub {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] :
has_sub (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_group {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] :
add_group (matrix m n α)
Equations
source
@[protected, instance]
def matrix.add_comm_group {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_group α] :
add_comm_group (matrix m n α)
Equations
source
@[protected, instance]
def matrix.unique {m : Type u_2} {n : Type u_3} {α : Type v} [unique α] :
unique (matrix m n α)
Equations
source
@[protected, instance]
def matrix.subsingleton {m : Type u_2} {n : Type u_3} {α : Type v} [subsingleton α] :
subsingleton (matrix m n α)
source
@[protected, instance]
def matrix.nontrivial {m : Type u_2} {n : Type u_3} {α : Type v} [nonempty m] [nonempty n] [nontrivial α] :
nontrivial (matrix m n α)
source
@[protected, instance]
def matrix.has_scalar {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_scalar R α] :
has_scalar R (matrix m n α)
Equations
source
@[protected, instance]
def matrix.smul_comm_class {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [has_scalar R α] [has_scalar S α] [smul_comm_class R S α] :
smul_comm_class R S (matrix m n α)
source
@[protected, instance]
def matrix.is_scalar_tower {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [has_scalar R S] [has_scalar R α] [has_scalar S α] [is_scalar_tower R S α] :
is_scalar_tower R S (matrix m n α)
source
@[protected, instance]
def matrix.is_central_scalar {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_scalar R α] [has_scalar Rᵐᵒᵖ α] [is_central_scalar R α] :
is_central_scalar R (matrix m n α)
source
@[protected, instance]
def matrix.mul_action {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [monoid R] [mul_action R α] :
mul_action R (matrix m n α)
Equations
source
@[protected, instance]
def matrix.distrib_mul_action {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [monoid R] [add_monoid α] [distrib_mul_action R α] :
distrib_mul_action R (matrix m n α)
Equations
source
@[protected, instance]
def matrix.module {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [add_comm_monoid α] [module R α] :
module R (matrix m n α)
Equations
source
@[simp]
theorem matrix.map_zero {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_zero α] [has_zero β] (f : α → β) (h : f 0 = 0) :
0.map f = 0
source
theorem matrix.map_add {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂) (M N : matrix m n α) :
(M + N).map f = M.map f + N.map f
source
theorem matrix.map_sub {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_sub α] [has_sub β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂) (M N : matrix m n α) :
(M - N).map f = M.map f - N.map f
source
theorem matrix.map_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [has_scalar R α] [has_scalar R β] (f : α → β) (r : R) (hf : ∀ (a : α), f (r • a) = r • f a) (M : matrix m n α) :
(r • M).map f = r • M.map f
source
theorem is_smul_regular.matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [has_scalar R S] {k : R} (hk : is_smul_regular S k) :
is_smul_regular (matrix m n S) k
source
theorem is_left_regular.matrix {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] {k : α} (hk : is_left_regular k) :
is_smul_regular (matrix m n α) k
source
theorem matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : Type v} [is_empty m] :
subsingleton (matrix m n α)
source
theorem matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : Type v} [is_empty n] :
subsingleton (matrix m n α)
source
def matrix.diagonal {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (d : n → α) :
matrix n n α

diagonal d is the square matrix such that (diagonal d) i i = d i and (diagonal d) i j = 0 if i ≠ j.

Note that bundled versions exist as:

Equations
source
@[simp]
theorem matrix.diagonal_apply_eq {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] {d : n → α} (i : n) :
matrix.diagonal d i i = d i
source
@[simp]
theorem matrix.diagonal_apply_ne {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] {d : n → α} {i j : n} (h : i ≠ j) :
matrix.diagonal d i j = 0
source
theorem matrix.diagonal_apply_ne' {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] {d : n → α} {i j : n} (h : j ≠ i) :
matrix.diagonal d i j = 0
source
theorem matrix.diagonal_injective {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] :
function.injective matrix.diagonal
source
@[simp]
theorem matrix.diagonal_zero {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] :
matrix.diagonal (λ (_x : n), 0) = 0
source
@[simp]
theorem matrix.diagonal_transpose {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (v : n → α) :
(matrix.diagonal v)ᵀ = matrix.diagonal v
source
@[simp]
theorem matrix.diagonal_add {n : Type u_3} {α : Type v} [decidable_eq n] [add_zero_class α] (d₁ d₂ : n → α) :
matrix.diagonal d₁ + matrix.diagonal d₂ = matrix.diagonal (λ (i : n), d₁ i + d₂ i)
source
@[simp]
theorem matrix.diagonal_smul {n : Type u_3} {R : Type u_7} {α : Type v} [decidable_eq n] [monoid R] [add_monoid α] [distrib_mul_action R α] (r : R) (d : n → α) :
matrix.diagonal (r • d) = r • matrix.diagonal d
source
def matrix.diagonal_add_monoid_hom (n : Type u_3) (α : Type v) [decidable_eq n] [add_zero_class α] :
(n → α) →+ matrix n n α

matrix.diagonal as an add_monoid_hom.

Equations
source
@[simp]
theorem matrix.diagonal_add_monoid_hom_apply (n : Type u_3) (α : Type v) [decidable_eq n] [add_zero_class α] (d : n → α) :
⇑(matrix.diagonal_add_monoid_hom n α) d = matrix.diagonal d
source
def matrix.diagonal_linear_map (n : Type u_3) (R : Type u_7) (α : Type v) [decidable_eq n] [semiring R] [add_comm_monoid α] [module R α] :
(n → α) →ₗ[R] matrix n n α

matrix.diagonal as a linear_map.

Equations
source
@[simp]
theorem matrix.diagonal_linear_map_apply (n : Type u_3) (R : Type u_7) (α : Type v) [decidable_eq n] [semiring R] [add_comm_monoid α] [module R α] (ᾰ : n → α) :
⇑(matrix.diagonal_linear_map n R α) ᾰ = (matrix.diagonal_add_monoid_hom n α).to_fun ᾰ
source
@[simp]
theorem matrix.diagonal_map {n : Type u_3} {α : Type v} {β : Type w} [decidable_eq n] [has_zero α] [has_zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :
(matrix.diagonal d).map f = matrix.diagonal (λ (m : n), f (d m))
source
@[simp]
theorem matrix.diagonal_conj_transpose {n : Type u_3} {α : Type v} [decidable_eq n] [semiring α] [star_ring α] (v : n → α) :
(matrix.diagonal v)ᴴ = matrix.diagonal (star v)
source
@[protected, instance]
def matrix.has_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
has_one (matrix n n α)
Equations
source
@[simp]
theorem matrix.diagonal_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
matrix.diagonal (λ (_x : n), 1) = 1
source
theorem matrix.one_apply {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {i j : n} :
1 i j = ite (i = j) 1 0
source
@[simp]
theorem matrix.one_apply_eq {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] (i : n) :
1 i i = 1
source
@[simp]
theorem matrix.one_apply_ne {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {i j : n} :
i ≠ j → 1 i j = 0
source
theorem matrix.one_apply_ne' {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {i j : n} :
j ≠ i → 1 i j = 0
source
@[simp]
theorem matrix.map_one {n : Type u_3} {α : Type v} {β : Type w} [decidable_eq n] [has_zero α] [has_one α] [has_zero β] [has_one β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
1.map f = 1
source
theorem matrix.one_eq_pi_single {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {i j : n} :
1 i j = pi.single i 1 j
source
@[simp]
theorem matrix.bit0_apply {m : Type u_2} {α : Type v} [has_add α] (M : matrix m m α) (i j : m) :
bit0 M i j = bit0 (M i j)
source
theorem matrix.bit1_apply {n : Type u_3} {α : 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))
source
@[simp]
theorem matrix.bit1_apply_eq {n : Type u_3} {α : Type v} [decidable_eq n] [add_monoid α] [has_one α] (M : matrix n n α) (i : n) :
bit1 M i i = bit1 (M i i)
source
@[simp]
theorem matrix.bit1_apply_ne {n : Type u_3} {α : Type v} [decidable_eq n] [add_monoid α] [has_one α] (M : matrix n n α) {i j : n} (h : i ≠ j) :
bit1 M i j = bit0 (M i j)
source
def matrix.dot_product {m : Type u_2} {α : Type v} [fintype m] [has_mul α] [add_comm_monoid α] (v w : m → α) :
α

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

Equations
source
theorem matrix.dot_product_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [non_unital_semiring α] (u : m → α) (w : n → α) (v : matrix m n α) :
(λ (j : n), u ⬝ᵥ λ (i : m), v i j) ⬝ᵥ w = u ⬝ᵥ λ (i : m), v i ⬝ᵥ w
source
theorem matrix.dot_product_comm {m : Type u_2} {α : Type v} [fintype m] [comm_semiring α] (v w : m → α) :
v ⬝ᵥ w = w ⬝ᵥ v
source
@[simp]
theorem matrix.dot_product_punit {α : Type v} [add_comm_monoid α] [has_mul α] (v w : punit → α) :
v ⬝ᵥ w = (v punit.star) * w punit.star
source
@[simp]
theorem matrix.dot_product_zero {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (v : m → α) :
v ⬝ᵥ 0 = 0
source
@[simp]
theorem matrix.dot_product_zero' {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (v : m → α) :
(v ⬝ᵥ λ (_x : m), 0) = 0
source
@[simp]
theorem matrix.zero_dot_product {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (v : m → α) :
0 ⬝ᵥ v = 0
source
@[simp]
theorem matrix.zero_dot_product' {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (v : m → α) :
(λ (_x : m), 0) ⬝ᵥ v = 0
source
@[simp]
theorem matrix.add_dot_product {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (u v w : m → α) :
(u + v) ⬝ᵥ w = u ⬝ᵥ w + v ⬝ᵥ w
source
@[simp]
theorem matrix.dot_product_add {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (u v w : m → α) :
u ⬝ᵥ (v + w) = u ⬝ᵥ v + u ⬝ᵥ w
source
@[simp]
theorem matrix.diagonal_dot_product {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring α] (v w : m → α) (i : m) :
matrix.diagonal v i ⬝ᵥ w = (v i) * w i
source
@[simp]
theorem matrix.dot_product_diagonal {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring α] (v w : m → α) (i : m) :
v ⬝ᵥ matrix.diagonal w i = (v i) * w i
source
@[simp]
theorem matrix.dot_product_diagonal' {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring α] (v w : m → α) (i : m) :
(v ⬝ᵥ λ (j : m), matrix.diagonal w j i) = (v i) * w i
source
@[simp]
theorem matrix.single_dot_product {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring α] (v : m → α) (x : α) (i : m) :
pi.single i x ⬝ᵥ v = x * v i
source
@[simp]
theorem matrix.dot_product_single {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring α] (v : m → α) (x : α) (i : m) :
v ⬝ᵥ pi.single i x = (v i) * x
source
@[simp]
theorem matrix.neg_dot_product {m : Type u_2} {α : Type v} [fintype m] [ring α] (v w : m → α) :
-v ⬝ᵥ w = -(v ⬝ᵥ w)
source
@[simp]
theorem matrix.dot_product_neg {m : Type u_2} {α : Type v} [fintype m] [ring α] (v w : m → α) :
v ⬝ᵥ -w = -(v ⬝ᵥ w)
source
@[simp]
theorem matrix.sub_dot_product {m : Type u_2} {α : Type v} [fintype m] [ring α] (u v w : m → α) :
(u - v) ⬝ᵥ w = u ⬝ᵥ w - v ⬝ᵥ w
source
@[simp]
theorem matrix.dot_product_sub {m : Type u_2} {α : Type v} [fintype m] [ring α] (u v w : m → α) :
u ⬝ᵥ (v - w) = u ⬝ᵥ v - u ⬝ᵥ w
source
@[simp]
theorem matrix.smul_dot_product {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [monoid R] [has_mul α] [add_comm_monoid α] [distrib_mul_action R α] [is_scalar_tower R α α] (x : R) (v w : m → α) :
x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
source
@[simp]
theorem matrix.dot_product_smul {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [monoid R] [has_mul α] [add_comm_monoid α] [distrib_mul_action R α] [smul_comm_class R α α] (x : R) (v w : m → α) :
v ⬝ᵥ x • w = x • (v ⬝ᵥ w)
source
theorem matrix.star_dot_product_star {m : Type u_2} {α : Type v} [fintype m] [semiring α] [star_ring α] (v w : m → α) :
star v ⬝ᵥ star w = star (w ⬝ᵥ v)
source
theorem matrix.star_dot_product {m : Type u_2} {α : Type v} [fintype m] [semiring α] [star_ring α] (v w : m → α) :
star v ⬝ᵥ w = star (star w ⬝ᵥ v)
source
theorem matrix.dot_product_star {m : Type u_2} {α : Type v} [fintype m] [semiring α] [star_ring α] (v w : m → α) :
v ⬝ᵥ star w = star (w ⬝ᵥ star v)
source
@[protected]
def matrix.mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [has_mul α] [add_comm_monoid α] (M : matrix l m α) (N : matrix m n α) :
matrix l n α

M ⬝ N is the usual product of matrices M and N, i.e. we have that (M ⬝ N) i k is the dot product of the i-th row of M by the k-th column of N. This is currently only defined when m is finite.

Equations
  • M ⬝ N = λ (i : l) (k : n), (λ (j : m), M i j) ⬝ᵥ λ (j : m), N j k
source
theorem matrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [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
source
@[protected, instance]
def matrix.has_mul {n : Type u_3} {α : Type v} [fintype n] [has_mul α] [add_comm_monoid α] :
has_mul (matrix n n α)
Equations
source
@[simp]
theorem matrix.mul_eq_mul {n : Type u_3} {α : Type v} [fintype n] [has_mul α] [add_comm_monoid α] (M N : matrix n n α) :
M * N = M ⬝ N
source
theorem matrix.mul_apply' {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [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) ⬝ᵥ λ (j : m), N j k
source
@[simp]
theorem matrix.diagonal_neg {n : Type u_3} {α : Type v} [decidable_eq n] [add_group α] (d : n → α) :
-matrix.diagonal d = matrix.diagonal (λ (i : n), -d i)
source
theorem matrix.sum_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [add_comm_monoid α] (i : m) (j : n) (s : finset β) (g : β → matrix m n α) :
(∑ (c : β) in s, g c) i j = ∑ (c : β) in s, g c i j
source
@[protected, simp]
theorem matrix.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (M : matrix m n α) :
M ⬝ 0 = 0
source
@[protected, simp]
theorem matrix.zero_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (M : matrix m n α) :
0 ⬝ M = 0
source
@[protected]
theorem matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (L : matrix m n α) (M N : matrix n o α) :
L ⬝ (M + N) = L ⬝ M + L ⬝ N
source
@[protected]
theorem matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (L M : matrix l m α) (N : matrix m n α) :
(L + M) ⬝ N = L ⬝ N + M ⬝ N
source
@[protected, instance]
def matrix.non_unital_non_assoc_semiring {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] :
non_unital_non_assoc_semiring (matrix n n α)
Equations
source
@[simp]
theorem matrix.diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] [decidable_eq m] (d : m → α) (M : matrix m n α) (i : m) (j : n) :
(matrix.diagonal d ⬝ M) i j = (d i) * M i j
source
@[simp]
theorem matrix.mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] [decidable_eq n] (d : n → α) (M : matrix m n α) (i : m) (j : n) :
(M ⬝ matrix.diagonal d) i j = (M i j) * d j
source
@[simp]
theorem matrix.diagonal_mul_diagonal {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] [decidable_eq n] (d₁ d₂ : n → α) :
matrix.diagonal d₁ ⬝ matrix.diagonal d₂ = matrix.diagonal (λ (i : n), (d₁ i) * d₂ i)
source
theorem matrix.diagonal_mul_diagonal' {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] [decidable_eq n] (d₁ d₂ : n → α) :
(matrix.diagonal d₁) * matrix.diagonal d₂ = matrix.diagonal (λ (i : n), (d₁ i) * d₂ i)
source
def matrix.add_monoid_hom_mul_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (M : matrix l m α) :
matrix m n α →+ matrix l n α

Left multiplication by a matrix, as an add_monoid_hom from matrices to matrices.

Equations
source
@[simp]
theorem matrix.add_monoid_hom_mul_left_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (M : matrix l m α) (x : matrix m n α) :
⇑(M.add_monoid_hom_mul_left) x = M ⬝ x
source
@[simp]
theorem matrix.add_monoid_hom_mul_right_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (M : matrix m n α) (x : matrix l m α) :
⇑(M.add_monoid_hom_mul_right) x = x ⬝ M
source
def matrix.add_monoid_hom_mul_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (M : matrix m n α) :
matrix l m α →+ matrix l n α

Right multiplication by a matrix, as an add_monoid_hom from matrices to matrices.

Equations
source
@[protected]
theorem matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [non_unital_non_assoc_semiring α] [fintype m] (s : finset β) (f : β → matrix l m α) (M : matrix m n α) :
(∑ (a : β) in s, f a) ⬝ M = ∑ (a : β) in s, f a ⬝ M
source
@[protected]
theorem matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [non_unital_non_assoc_semiring α] [fintype m] (s : finset β) (f : β → matrix m n α) (M : matrix l m α) :
M ⬝ ∑ (a : β) in s, f a = ∑ (a : β) in s, M ⬝ f a
source
@[protected, simp]
theorem matrix.one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_assoc_semiring α] [fintype m] [decidable_eq m] (M : matrix m n α) :
1 ⬝ M = M
source
@[protected, simp]
theorem matrix.mul_one {m : Type u_2} {n : Type u_3} {α : Type v} [non_assoc_semiring α] [fintype n] [decidable_eq n] (M : matrix m n α) :
M ⬝ 1 = M
source
@[protected, instance]
def matrix.non_assoc_semiring {n : Type u_3} {α : Type v} [non_assoc_semiring α] [fintype n] [decidable_eq n] :
non_assoc_semiring (matrix n n α)
Equations
source
@[simp]
theorem matrix.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [non_assoc_semiring α] [fintype n] {L : matrix m n α} {M : matrix n o α} [non_assoc_semiring β] {f : α →+* β} :
(L ⬝ M).map ⇑f = L.map ⇑f ⬝ M.map ⇑f
source
def matrix.diagonal_ring_hom (n : Type u_3) (α : Type v) [non_assoc_semiring α] [fintype n] [decidable_eq n] :
(n → α) →+* matrix n n α

matrix.diagonal as a ring_hom.

Equations
source
@[simp]
theorem matrix.diagonal_ring_hom_apply (n : Type u_3) (α : Type v) [non_assoc_semiring α] [fintype n] [decidable_eq n] (d : n → α) :
⇑(matrix.diagonal_ring_hom n α) d = matrix.diagonal d
source
@[protected]
theorem matrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_semiring α] [fintype m] [fintype n] (L : matrix l m α) (M : matrix m n α) (N : matrix n o α) :
L ⬝ M ⬝ N = L ⬝ (M ⬝ N)
source
@[protected, instance]
def matrix.non_unital_semiring {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype n] :
non_unital_semiring (matrix n n α)
Equations
source
@[protected, instance]
def matrix.semiring {n : Type u_3} {α : Type v} [semiring α] [fintype n] [decidable_eq n] :
semiring (matrix n n α)
Equations
source
@[simp]
theorem matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [ring α] [fintype n] (M : matrix m n α) (N : matrix n o α) :
-M ⬝ N = -(M ⬝ N)
source
@[simp]
theorem matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [ring α] [fintype n] (M : matrix m n α) (N : matrix n o α) :
M ⬝ -N = -(M ⬝ N)
source
@[protected]
theorem matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [ring α] [fintype n] (M M' : matrix m n α) (N : matrix n o α) :
(M - M') ⬝ N = M ⬝ N - M' ⬝ N
source
@[protected]
theorem matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [ring α] [fintype n] (M : matrix m n α) (N N' : matrix n o α) :
M ⬝ (N - N') = M ⬝ N - M ⬝ N'
source
@[protected, instance]
def matrix.ring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] [ring α] :
ring (matrix n n α)
Equations
source
theorem matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [semiring α] [fintype m] [decidable_eq m] (M : matrix m n α) (a : α) :
a • M = matrix.diagonal (λ (_x : m), a) ⬝ M
source
@[simp]
theorem matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring α] [fintype n] [monoid R] [distrib_mul_action R α] [is_scalar_tower R α α] (a : R) (M : matrix m n α) (N : matrix n l α) :
(a • M) ⬝ N = a • M ⬝ N
source
@[protected, instance]
def matrix.semiring.is_scalar_tower {n : Type u_3} {R : Type u_7} {α : Type v} [semiring α] [fintype n] [monoid R] [distrib_mul_action R α] [is_scalar_tower R α α] :
is_scalar_tower R (matrix n n α) (matrix n n α)

This instance enables use with smul_mul_assoc.

source
@[simp]
theorem matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring α] [fintype n] [monoid R] [distrib_mul_action R α] [smul_comm_class R α α] (M : matrix m n α) (a : R) (N : matrix n l α) :
M ⬝ (a • N) = a • M ⬝ N
source
@[protected, instance]
def matrix.semiring.smul_comm_class {n : Type u_3} {R : Type u_7} {α : Type v} [semiring α] [fintype n] [monoid R] [distrib_mul_action R α] [smul_comm_class R α α] :
smul_comm_class R (matrix n n α) (matrix n n α)

This instance enables use with mul_smul_comm.

source
@[simp]
theorem matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [semiring α] [fintype n] (M : matrix m n α) (N : matrix n o α) (a : α) :
(λ (i : m) (j : n), a * M i j) ⬝ N = a • M ⬝ N
source
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
source
@[simp]
theorem matrix.coe_scalar {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] :
⇑(matrix.scalar n) = λ (a : α), a • 1
source
theorem matrix.scalar_apply_eq {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] (a : α) (i : n) :
⇑(matrix.scalar n) a i i = a
source
theorem matrix.scalar_apply_ne {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] (a : α) (i j : n) (h : i ≠ j) :
⇑(matrix.scalar n) a i j = 0
source
theorem matrix.scalar_inj {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] [nonempty n] {r s : α} :
⇑(matrix.scalar n) r = ⇑(matrix.scalar n) s ↔ r = s
source
theorem matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [comm_semiring α] [fintype n] [decidable_eq n] (M : matrix m n α) (a : α) :
a • M = M ⬝ matrix.diagonal (λ (_x : n), a)
source
@[simp]
theorem matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [comm_semiring α] [fintype n] (M : matrix m n α) (N : matrix n o α) (a : α) :
(M ⬝ λ (i : n) (j : o), a * N i j) = a • M ⬝ N
source
theorem matrix.scalar.commute {n : Type u_3} {α : Type v} [comm_semiring α] [fintype n] [decidable_eq n] (r : α) (M : matrix n n α) :
commute (⇑(matrix.scalar n) r) M
source
@[protected, instance]
def matrix.algebra {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] :
algebra R (matrix n n α)
Equations
source
theorem matrix.algebra_map_matrix_apply {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] {r : R} {i j : n} :
⇑(algebra_map R (matrix n n α)) r i j = ite (i = j) (⇑(algebra_map R α) r) 0
source
theorem matrix.algebra_map_eq_diagonal {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] (r : R) :
⇑(algebra_map R (matrix n n α)) r = matrix.diagonal (⇑(algebra_map R (n → α)) r)
source
@[simp]
theorem matrix.algebra_map_eq_smul {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] [comm_semiring R] (r : R) :
⇑(algebra_map R (matrix n n R)) r = r • 1
source
theorem matrix.algebra_map_eq_diagonal_ring_hom {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] :
algebra_map R (matrix n n α) = (matrix.diagonal_ring_hom n α).comp (algebra_map R (n → α))
source
@[simp]
theorem matrix.map_algebra_map {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f (⇑(algebra_map R α) r) = ⇑(algebra_map R β) r) :
(⇑(algebra_map R (matrix n n α)) r).map f = ⇑(algebra_map R (matrix n n β)) r
source
def matrix.diagonal_alg_hom {n : Type u_3} (R : Type u_7) {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] :
(n → α) →ₐ[R] matrix n n α

matrix.diagonal as an alg_hom.

Equations
source
@[simp]
theorem matrix.diagonal_alg_hom_apply {n : Type u_3} (R : Type u_7) {α : Type v} [fintype n] [decidable_eq n] [comm_semiring R] [semiring α] [algebra R α] (d : n → α) :
⇑(matrix.diagonal_alg_hom R) d = matrix.diagonal d

Bundled versions of matrix.map #

source
def equiv.map_matrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) :
matrix m n α ≃ matrix m n β

The equiv between spaces of matrices induced by an equiv between their coefficients. This is matrix.map as an equiv.

Equations
source
@[simp]
theorem equiv.map_matrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) (M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} :
(equiv.refl α).map_matrix = equiv.refl (matrix m n α)
source
@[simp]
theorem equiv.map_matrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) :
f.map_matrix.symm = f.symm.map_matrix
source
@[simp]
theorem equiv.map_matrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} (f : α ≃ β) (g : β ≃ γ) :
f.map_matrix.trans g.map_matrix = (f.trans g).map_matrix
source
def add_monoid_hom.map_matrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [add_zero_class α] [add_zero_class β] (f : α →+ β) :
matrix m n α →+ matrix m n β

The add_monoid_hom between spaces of matrices induced by an add_monoid_hom between their coefficients. This is matrix.map as an add_monoid_hom.

Equations
source
@[simp]
theorem add_monoid_hom.map_matrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [add_zero_class α] [add_zero_class β] (f : α →+ β) (M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem add_monoid_hom.map_matrix_id {m : Type u_2} {n : Type u_3} {α : Type v} [add_zero_class α] :
(add_monoid_hom.id α).map_matrix = add_monoid_hom.id (matrix m n α)
source
@[simp]
theorem add_monoid_hom.map_matrix_comp {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [add_zero_class α] [add_zero_class β] [add_zero_class γ] (f : β →+ γ) (g : α →+ β) :
f.map_matrix.comp g.map_matrix = (f.comp g).map_matrix
source
def add_equiv.map_matrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α ≃+ β) :
matrix m n α ≃+ matrix m n β

The add_equiv between spaces of matrices induced by an add_equiv between their coefficients. This is matrix.map as an add_equiv.

Equations
source
@[simp]
theorem add_equiv.map_matrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α ≃+ β) (M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem add_equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
(add_equiv.refl α).map_matrix = add_equiv.refl (matrix m n α)
source
@[simp]
theorem add_equiv.map_matrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α ≃+ β) :
f.map_matrix.symm = f.symm.map_matrix
source
@[simp]
theorem add_equiv.map_matrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} [has_add α] [has_add β] [has_add γ] (f : α ≃+ β) (g : β ≃+ γ) :
f.map_matrix.trans g.map_matrix = (f.trans g).map_matrix
source
def linear_map.map_matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (f : α →ₗ[R] β) :
matrix m n α →ₗ[R] matrix m n β

The linear_map between spaces of matrices induced by a linear_map between their coefficients. This is matrix.map as a linear_map.

Equations
source
@[simp]
theorem linear_map.map_matrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (f : α →ₗ[R] β) (M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem linear_map.map_matrix_id {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [add_comm_monoid α] [module R α] :
linear_map.id.map_matrix = linear_map.id
source
@[simp]
theorem linear_map.map_matrix_comp {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [module R α] [module R β] [module R γ] (f : β →ₗ[R] γ) (g : α →ₗ[R] β) :
f.map_matrix.comp g.map_matrix = (f.comp g).map_matrix
source
def linear_equiv.map_matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (f : α ≃ₗ[R] β) :
matrix m n α ≃ₗ[R] matrix m n β

The linear_equiv between spaces of matrices induced by an linear_equiv between their coefficients. This is matrix.map as an linear_equiv.

Equations
source
@[simp]
theorem linear_equiv.map_matrix_apply {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (f : α ≃ₗ[R] β) (M : matrix m n α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem linear_equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [add_comm_monoid α] [module R α] :
(linear_equiv.refl R α).map_matrix = linear_equiv.refl R (matrix m n α)
source
@[simp]
theorem linear_equiv.map_matrix_symm {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [module R α] [module R β] (f : α ≃ₗ[R] β) :
f.map_matrix.symm = f.symm.map_matrix
source
@[simp]
theorem linear_equiv.map_matrix_trans {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [semiring R] [add_comm_monoid α] [add_comm_monoid β] [add_comm_monoid γ] [module R α] [module R β] [module R γ] (f : α ≃ₗ[R] β) (g : β ≃ₗ[R] γ) :
f.map_matrix.trans g.map_matrix = (f.trans g).map_matrix
source
def ring_hom.map_matrix {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] (f : α →+* β) :
matrix m m α →+* matrix m m β

The ring_hom between spaces of square matrices induced by a ring_hom between their coefficients. This is matrix.map as a ring_hom.

Equations
source
@[simp]
theorem ring_hom.map_matrix_apply {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] (f : α →+* β) (M : matrix m m α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem ring_hom.map_matrix_id {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_assoc_semiring α] :
(ring_hom.id α).map_matrix = ring_hom.id (matrix m m α)
source
@[simp]
theorem ring_hom.map_matrix_comp {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] [non_assoc_semiring γ] (f : β →+* γ) (g : α →+* β) :
f.map_matrix.comp g.map_matrix = (f.comp g).map_matrix
source
def ring_equiv.map_matrix {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] (f : α ≃+* β) :
matrix m m α ≃+* matrix m m β

The ring_equiv between spaces of square matrices induced by a ring_equiv between their coefficients. This is matrix.map as a ring_equiv.

Equations
source
@[simp]
theorem ring_equiv.map_matrix_apply {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] (f : α ≃+* β) (M : matrix m m α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem ring_equiv.map_matrix_refl {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_assoc_semiring α] :
(ring_equiv.refl α).map_matrix = ring_equiv.refl (matrix m m α)
source
@[simp]
theorem ring_equiv.map_matrix_symm {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] (f : α ≃+* β) :
f.map_matrix.symm = f.symm.map_matrix
source
@[simp]
theorem ring_equiv.map_matrix_trans {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] [non_assoc_semiring α] [non_assoc_semiring β] [non_assoc_semiring γ] (f : α ≃+* β) (g : β ≃+* γ) :
f.map_matrix.trans g.map_matrix = (f.trans g).map_matrix
source
def alg_hom.map_matrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (f : α →ₐ[R] β) :
matrix m m α →ₐ[R] matrix m m β

The alg_hom between spaces of square matrices induced by a alg_hom between their coefficients. This is matrix.map as a alg_hom.

Equations
source
@[simp]
theorem alg_hom.map_matrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (f : α →ₐ[R] β) (M : matrix m m α) :
⇑(f.map_matrix) M = M.map ⇑f
source
@[simp]
theorem alg_hom.map_matrix_id {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [algebra R α] :
(alg_hom.id R α).map_matrix = alg_hom.id R (matrix m m α)
source
@[simp]
theorem alg_hom.map_matrix_comp {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [semiring γ] [algebra R α] [algebra R β] [algebra R γ] (f : β →ₐ[R] γ) (g : α →ₐ[R] β) :
f.map_matrix.comp g.map_matrix = (f.comp g).map_matrix
source
@[simp]
theorem alg_equiv.map_matrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (f : α ≃ₐ[R] β) (M : matrix m m α) :
⇑(f.map_matrix) M = M.map ⇑f
source
def alg_equiv.map_matrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (f : α ≃ₐ[R] β) :
matrix m m α ≃ₐ[R] matrix m m β

The alg_equiv between spaces of square matrices induced by a alg_equiv between their coefficients. This is matrix.map as a alg_equiv.

Equations
source
@[simp]
theorem alg_equiv.map_matrix_refl {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [algebra R α] :
alg_equiv.refl.map_matrix = alg_equiv.refl
source
@[simp]
theorem alg_equiv.map_matrix_symm {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [algebra R α] [algebra R β] (f : α ≃ₐ[R] β) :
f.map_matrix.symm = f.symm.map_matrix
source
@[simp]
theorem alg_equiv.map_matrix_trans {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] [comm_semiring R] [semiring α] [semiring β] [semiring γ] [algebra R α] [algebra R β] [algebra R γ] (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) :
f.map_matrix.trans g.map_matrix = (f.trans g).map_matrix
source
def matrix.vec_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] (w : m → α) (v : n → α) :
matrix m n α

For two vectors w and v, vec_mul_vec w v i j is defined to be w i * v j. Put another way, vec_mul_vec w v is exactly col w ⬝ row v.

Equations
source
def matrix.mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (M : matrix m n α) (v : n → α) :
m → α

mul_vec M v is the matrix-vector product of M and v, where v is seen as a column matrix. Put another way, mul_vec M v is the vector whose entries are those of M ⬝ col v (see col_mul_vec).

Equations
source
def matrix.vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (v : m → α) (M : matrix m n α) :
n → α

vec_mul v M is the vector-matrix product of v and M, where v is seen as a row matrix. Put another way, vec_mul v M is the vector whose entries are those of row v ⬝ M (see row_vec_mul).

Equations
source
def matrix.mul_vec.add_monoid_hom_left {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (v : n → α) :
matrix m n α →+ m → α

Left multiplication by a matrix, as an add_monoid_hom from vectors to vectors.

Equations
source
@[simp]
theorem matrix.mul_vec.add_monoid_hom_left_apply {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (v : n → α) (M : matrix m n α) (ᾰ : m) :
⇑(matrix.mul_vec.add_monoid_hom_left v) M ᾰ = M.mul_vec v ᾰ
source
theorem matrix.mul_vec_diagonal {m : Type u_2} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] [decidable_eq m] (v w : m → α) (x : m) :
(matrix.diagonal v).mul_vec w x = (v x) * w x
source
theorem matrix.vec_mul_diagonal {m : Type u_2} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] [decidable_eq m] (v w : m → α) (x : m) :
matrix.vec_mul v (matrix.diagonal w) x = (v x) * w x
source
theorem matrix.dot_product_mul_vec {m : Type u_2} {n : Type u_3} {R : Type u_7} [fintype n] [fintype m] [non_unital_semiring R] (v : m → R) (A : matrix m n R) (w : n → R) :
v ⬝ᵥ A.mul_vec w = matrix.vec_mul v A ⬝ᵥ w

Associate the dot product of mul_vec to the left.

source
@[simp]
theorem matrix.mul_vec_zero {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (A : matrix m n α) :
A.mul_vec 0 = 0
source
@[simp]
theorem matrix.zero_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (A : matrix m n α) :
matrix.vec_mul 0 A = 0
source
@[simp]
theorem matrix.zero_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (v : n → α) :
0.mul_vec v = 0
source
@[simp]
theorem matrix.vec_mul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (v : m → α) :
matrix.vec_mul v 0 = 0
source
theorem matrix.vec_mul_vec_eq {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] (w : m → α) (v : n → α) :
matrix.vec_mul_vec w v = matrix.col w ⬝ matrix.row v
source
theorem matrix.smul_mul_vec_assoc {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] [monoid R] [distrib_mul_action R α] [is_scalar_tower R α α] (a : R) (A : matrix m n α) (b : n → α) :
(a • A).mul_vec b = a • A.mul_vec b
source
theorem matrix.mul_vec_add {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (A : matrix m n α) (x y : n → α) :
A.mul_vec (x + y) = A.mul_vec x + A.mul_vec y
source
theorem matrix.add_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype n] (A B : matrix m n α) (x : n → α) :
(A + B).mul_vec x = A.mul_vec x + B.mul_vec x
source
theorem matrix.vec_mul_add {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (A B : matrix m n α) (x : m → α) :
matrix.vec_mul x (A + B) = matrix.vec_mul x A + matrix.vec_mul x B
source
theorem matrix.add_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] (A : matrix m n α) (x y : m → α) :
matrix.vec_mul (x + y) A = matrix.vec_mul x A + matrix.vec_mul y A
source
theorem matrix.vec_mul_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [comm_semiring R] [semiring S] [algebra R S] (M : matrix n m S) (b : R) (v : n → S) :
matrix.vec_mul (b • v) M = b • matrix.vec_mul v M
source
theorem matrix.mul_vec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [comm_semiring R] [semiring S] [algebra R S] (M : matrix m n S) (b : R) (v : n → S) :
M.mul_vec (b • v) = b • M.mul_vec v
source
@[simp]
theorem matrix.vec_mul_vec_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_semiring α] [fintype n] [fintype m] (v : m → α) (M : matrix m n α) (N : matrix n o α) :
matrix.vec_mul (matrix.vec_mul v M) N = matrix.vec_mul v (M ⬝ N)
source
@[simp]
theorem matrix.mul_vec_mul_vec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_semiring α] [fintype n] [fintype o] (v : o → α) (M : matrix m n α) (N : matrix n o α) :
M.mul_vec (N.mul_vec v) = (M ⬝ N).mul_vec v
source
@[simp]
theorem matrix.one_mul_vec {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_assoc_semiring α] (v : m → α) :
1.mul_vec v = v
source
@[simp]
theorem matrix.vec_mul_one {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] [non_assoc_semiring α] (v : m → α) :
matrix.vec_mul v 1 = v
source
theorem matrix.neg_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [ring α] [fintype m] (v : m → α) (A : matrix m n α) :
matrix.vec_mul (-v) A = -matrix.vec_mul v A
source
theorem matrix.vec_mul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [ring α] [fintype m] (v : m → α) (A : matrix m n α) :
matrix.vec_mul v (-A) = -matrix.vec_mul v A
source
theorem matrix.neg_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [ring α] [fintype n] (v : n → α) (A : matrix m n α) :
(-A).mul_vec v = -A.mul_vec v
source
theorem matrix.mul_vec_neg {m : Type u_2} {n : Type u_3} {α : Type v} [ring α] [fintype n] (v : n → α) (A : matrix m n α) :
A.mul_vec (-v) = -A.mul_vec v
source
theorem matrix.mul_vec_smul_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [comm_semiring α] [fintype n] (A : matrix m n α) (b : n → α) (a : α) :
A.mul_vec (a • b) = a • A.mul_vec b
source
theorem matrix.mul_vec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [comm_semiring α] [fintype m] (A : matrix m n α) (x : m → α) :
Aᵀ.mul_vec x = matrix.vec_mul x A
source
theorem matrix.vec_mul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [comm_semiring α] [fintype n] (A : matrix m n α) (x : n → α) :
matrix.vec_mul x Aᵀ = A.mul_vec x
source
@[simp]
theorem matrix.transpose_apply {m : Type u_2} {n : Type u_3} {α : 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.

source
@[simp]
theorem matrix.transpose_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : matrix m n α) :
Mᵀᵀ = M
source
@[simp]
theorem matrix.transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
0ᵀ = 0
source
@[simp]
theorem matrix.transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
1ᵀ = 1
source
@[simp]
theorem matrix.transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] (M N : matrix m n α) :
(M + N)ᵀ = Mᵀ + Nᵀ
source
@[simp]
theorem matrix.transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] (M N : matrix m n α) :
(M - N)ᵀ = Mᵀ - Nᵀ
source
@[simp]
theorem matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [comm_semiring α] [fintype n] (M : matrix m n α) (N : matrix n l α) :
(M ⬝ N)ᵀ = Nᵀ ⬝ Mᵀ
source
@[simp]
theorem matrix.transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_1} [has_scalar R α] (c : R) (M : matrix m n α) :
(c • M)ᵀ = c • Mᵀ
source
@[simp]
theorem matrix.transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] (M : matrix m n α) :
(-M)ᵀ = -Mᵀ
source
theorem matrix.transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : matrix m n α} :
Mᵀ.map f = (M.map f)ᵀ
source
@[simp]
theorem matrix.transpose_add_equiv_apply {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] (M : matrix m n α) :
⇑matrix.transpose_add_equiv M = Mᵀ
source
def matrix.transpose_add_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
matrix m n α ≃+ matrix n m α

matrix.transpose as an add_equiv

Equations
source
@[simp]
theorem matrix.transpose_add_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
matrix.transpose_add_equiv.symm = matrix.transpose_add_equiv
source
theorem matrix.transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] (l : list (matrix m n α)) :
(l.sum)ᵀ = (list.map matrix.transpose l).sum
source
theorem matrix.transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] (s : multiset (matrix m n α)) :
(s.sum)ᵀ = (multiset.map matrix.transpose s).sum
source
theorem matrix.transpose_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] {ι : Type u_1} (s : finset ι) (M : ι → matrix m n α) :
(∑ (i : ι) in s, M i)ᵀ = ∑ (i : ι) in s, (M i)ᵀ
source
def matrix.transpose_ring_equiv {m : Type u_2} {α : Type v} [comm_semiring α] [fintype m] :
matrix m m α ≃+* (matrix m m α)ᵐᵒᵖ

matrix.transpose as a ring_equiv to the opposite ring

Equations
source
@[simp]
theorem matrix.transpose_ring_equiv_apply {m : Type u_2} {α : Type v} [comm_semiring α] [fintype m] (M : matrix m m α) :
⇑matrix.transpose_ring_equiv M = mul_opposite.op Mᵀ
source
@[simp]
theorem matrix.transpose_ring_equiv_symm_apply {m : Type u_2} {α : Type v} [comm_semiring α] [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
⇑(matrix.transpose_ring_equiv.symm) M = (mul_opposite.unop M)ᵀ
source
theorem matrix.transpose_list_prod {m : Type u_2} {α : Type v} [comm_semiring α] [fintype m] [decidable_eq m] (l : list (matrix m m α)) :
(l.prod)ᵀ = (list.map matrix.transpose l).reverse.prod
source
@[simp]
theorem matrix.conj_transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} [has_star α] (M : matrix m n α) (i : m) (j : n) :
Mᴴ j i = star (M i j)

Tell simp what the entries are in a conjugate transposed matrix.

Compare with mul_apply, diagonal_apply_eq, etc.

source
@[simp]
theorem matrix.conj_transpose_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [has_involutive_star α] (M : matrix m n α) :
Mᴴᴴ = M
source
@[simp]
theorem matrix.conj_transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [semiring α] [star_ring α] :
0ᴴ = 0
source
@[simp]
theorem matrix.conj_transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [semiring α] [star_ring α] :
1ᴴ = 1
source
@[simp]
theorem matrix.conj_transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] (M N : matrix m n α) :
(M + N)ᴴ = Mᴴ + Nᴴ
source
@[simp]
theorem matrix.conj_transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] [star_add_monoid α] (M N : matrix m n α) :
(M - N)ᴴ = Mᴴ - Nᴴ
source
@[simp]
theorem matrix.conj_transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} [comm_monoid α] [star_monoid α] (c : α) (M : matrix m n α) :
(c • M)ᴴ = star c • Mᴴ
source
@[simp]
theorem matrix.conj_transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [semiring α] [star_ring α] (M : matrix m n α) (N : matrix n l α) :
(M ⬝ N)ᴴ = Nᴴ ⬝ Mᴴ
source
@[simp]
theorem matrix.conj_transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [ring α] [star_ring α] (M : matrix m n α) :
(-M)ᴴ = -Mᴴ
source
@[simp]
theorem matrix.conj_transpose_add_equiv_apply {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] (M : matrix m n α) :
⇑matrix.conj_transpose_add_equiv M = Mᴴ
source
def matrix.conj_transpose_add_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] :
matrix m n α ≃+ matrix n m α

matrix.conj_transpose as an add_equiv

Equations
source
@[simp]
theorem matrix.conj_transpose_add_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] :
matrix.conj_transpose_add_equiv.symm = matrix.conj_transpose_add_equiv
source
theorem matrix.conj_transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] (l : list (matrix m n α)) :
(l.sum)ᴴ = (list.map matrix.conj_transpose l).sum
source
theorem matrix.conj_transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] [star_add_monoid α] (s : multiset (matrix m n α)) :
(s.sum)ᴴ = (multiset.map matrix.conj_transpose s).sum
source
theorem matrix.conj_transpose_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] [star_add_monoid α] {ι : Type u_1} (s : finset ι) (M : ι → matrix m n α) :
(∑ (i : ι) in s, M i)ᴴ = ∑ (i : ι) in s, (M i)ᴴ
source
def matrix.conj_transpose_ring_equiv {m : Type u_2} {α : Type v} [comm_semiring α] [star_ring α] [fintype m] :
matrix m m α ≃+* (matrix m m α)ᵐᵒᵖ

matrix.conj_transpose as a ring_equiv to the opposite ring

Equations
source
@[simp]
theorem matrix.conj_transpose_ring_equiv_apply {m : Type u_2} {α : Type v} [comm_semiring α] [star_ring α] [fintype m] (M : matrix m m α) :
⇑matrix.conj_transpose_ring_equiv M = mul_opposite.op Mᴴ
source
@[simp]
theorem matrix.conj_transpose_ring_equiv_symm_apply {m : Type u_2} {α : Type v} [comm_semiring α] [star_ring α] [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
⇑(matrix.conj_transpose_ring_equiv.symm) M = (mul_opposite.unop M)ᴴ
source
theorem matrix.conj_transpose_list_prod {m : Type u_2} {α : Type v} [comm_semiring α] [star_ring α] [fintype m] [decidable_eq m] (l : list (matrix m m α)) :
(l.prod)ᴴ = (list.map matrix.conj_transpose l).reverse.prod
source
@[protected, instance]
def matrix.has_star {n : Type u_3} {α : Type v} [has_star α] :
has_star (matrix n n α)

When α has a star operation, square matrices matrix n n α have a star operation equal to matrix.conj_transpose.

Equations
source
theorem matrix.star_eq_conj_transpose {m : Type u_2} {α : Type v} [has_star α] (M : matrix m m α) :
star M = Mᴴ
source
@[simp]
theorem matrix.star_apply {n : Type u_3} {α : Type v} [has_star α] (M : matrix n n α) (i j : n) :
star M i j = star (M j i)
source
@[protected, instance]
def matrix.has_involutive_star {n : Type u_3} {α : Type v} [has_involutive_star α] :
has_involutive_star (matrix n n α)
Equations
source
@[protected, instance]
def matrix.star_add_monoid {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] :
star_add_monoid (matrix n n α)

When α is a *-additive monoid, matrix.has_star is also a *-additive monoid.

Equations
source
@[protected, instance]
def matrix.star_ring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] [semiring α] [star_ring α] :
star_ring (matrix n n α)

When α is a *-(semi)ring, matrix.has_star is also a *-(semi)ring.

Equations
source
theorem matrix.star_mul {n : Type u_3} {α : Type v} [fintype n] [semiring α] [star_ring α] (M N : matrix n n α) :
star (M ⬝ N) = star N ⬝ star M

A version of star_mul for ⬝ instead of *.

source
def matrix.minor {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
matrix l o α

Given maps (r_reindex : l → m) and (c_reindex : o → n) reindexing the rows and columns of a matrix M : matrix m n α, the matrix M.minor r_reindex c_reindex : matrix l o α is defined by (M.minor r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j) for (i,j) : l × o. Note that the total number of row and columns does not have to be preserved.

Equations
  • A.minor r_reindex c_reindex = λ (i : l) (j : o), A (r_reindex i) (c_reindex j)
source
@[simp]
theorem matrix.minor_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i : l) (j : o) :
A.minor r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)
source
@[simp]
theorem matrix.minor_id_id {m : Type u_2} {n : Type u_3} {α : Type v} (A : matrix m n α) :
A.minor id id = A
source
@[simp]
theorem matrix.minor_minor {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_5} {o₂ : Type u_6} (A : matrix m n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) :
(A.minor r₁ c₁).minor r₂ c₂ = A.minor (r₁ ∘ r₂) (c₁ ∘ c₂)
source
@[simp]
theorem matrix.transpose_minor {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
(A.minor r_reindex c_reindex)ᵀ = Aᵀ.minor c_reindex r_reindex
source
@[simp]
theorem matrix.conj_transpose_minor {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_star α] (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
(A.minor r_reindex c_reindex)ᴴ = Aᴴ.minor c_reindex r_reindex
source
theorem matrix.minor_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_add α] (A B : matrix m n α) :
(A + B).minor = A.minor + B.minor
source
theorem matrix.minor_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_neg α] (A : matrix m n α) :
(-A).minor = -A.minor
source
theorem matrix.minor_sub {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_sub α] (A B : matrix m n α) :
(A - B).minor = A.minor - B.minor
source
@[simp]
theorem matrix.minor_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_zero α] :
0.minor = 0
source
theorem matrix.minor_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {R : Type u_5} [semiring R] [add_comm_monoid α] [module R α] (r : R) (A : matrix m n α) :
(r • A).minor = r • A.minor
source
theorem matrix.minor_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : matrix m n α) :
(A.map f).minor e₁ e₂ = (A.minor e₁ e₂).map f
source
theorem matrix.minor_diagonal {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [decidable_eq m] [decidable_eq l] (d : m → α) (e : l → m) (he : function.injective e) :
(matrix.diagonal d).minor e e = matrix.diagonal (d ∘ e)

Given a (m × m) diagonal matrix defined by a map d : m → α, if the reindexing map e is injective, then the resulting matrix is again diagonal.

source
theorem matrix.minor_one {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [has_one α] [decidable_eq m] [decidable_eq l] (e : l → m) (he : function.injective e) :
1.minor e e = 1
source
theorem matrix.minor_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [semiring α] {p : Type u_5} {q : Type u_6} (M : matrix m n α) (N : matrix 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.minors interaction with matrix.diagonal, 1, and matrix.mul for when the mappings are bundled.

source
@[simp]
theorem matrix.minor_diagonal_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [decidable_eq m] [decidable_eq l] (d : m → α) (e : l ↪ m) :
(matrix.diagonal d).minor ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
source
@[simp]
theorem matrix.minor_diagonal_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [decidable_eq m] [decidable_eq l] (d : m → α) (e : l ≃ m) :
(matrix.diagonal d).minor ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
source
@[simp]
theorem matrix.minor_one_embedding {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [has_one α] [decidable_eq m] [decidable_eq l] (e : l ↪ m) :
1.minor ⇑e ⇑e = 1
source
@[simp]
theorem matrix.minor_one_equiv {l : Type u_1} {m : Type u_2} {α : Type v} [has_zero α] [has_one α] [decidable_eq m] [decidable_eq l] (e : l ≃ m) :
1.minor ⇑e ⇑e = 1
source
@[simp]
theorem matrix.minor_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [semiring α] {p : Type u_5} {q : Type u_6} (M : matrix m n α) (N : matrix n p α) (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p) :
M.minor e₁ ⇑e₂ ⬝ N.minor ⇑e₂ e₃ = (M ⬝ N).minor e₁ e₃
source
theorem matrix.mul_minor_one {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [semiring α] [decidable_eq o] (e₁ : n ≃ o) (e₂ : l → o) (M : matrix m n α) :
M ⬝ 1.minor ⇑e₁ e₂ = M.minor id (⇑(e₁.symm) ∘ e₂)
source
theorem matrix.one_minor_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype m] [fintype o] [semiring α] [decidable_eq o] (e₁ : l → o) (e₂ : m ≃ o) (M : matrix m n α) :
1.minor e₁ ⇑e₂ ⬝ M = M.minor (⇑(e₂.symm) ∘ e₁) id
source
def matrix.reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) :
matrix m n α ≃ matrix l o α

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

Equations
source
@[simp]
theorem matrix.reindex_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : matrix m n α) :
⇑(matrix.reindex eₘ eₙ) M = M.minor ⇑(eₘ.symm) ⇑(eₙ.symm)
source
@[simp]
theorem matrix.reindex_refl_refl {m : Type u_2} {n : Type u_3} {α : Type v} (A : matrix m n α) :
⇑(matrix.reindex (equiv.refl m) (equiv.refl n)) A = A
source
@[simp]
theorem matrix.reindex_symm {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) :
(matrix.reindex eₘ eₙ).symm = matrix.reindex eₘ.symm eₙ.symm
source
@[simp]
theorem matrix.reindex_trans {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {l₂ : Type u_5} {o₂ : Type u_6} (eₘ : m ≃ l) (eₙ : n ≃ o) (eₘ₂ : l ≃ l₂) (eₙ₂ : o ≃ o₂) :
(matrix.reindex eₘ eₙ).trans (matrix.reindex eₘ₂ eₙ₂) = matrix.reindex (eₘ.trans eₘ₂) (eₙ.trans eₙ₂)
source
theorem matrix.transpose_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o) (M : matrix m n α) :
(⇑(matrix.reindex eₘ eₙ) M)ᵀ = ⇑(matrix.reindex eₙ eₘ) Mᵀ
source
theorem matrix.conj_transpose_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_star α] (eₘ : m ≃ l) (eₙ : n ≃ o) (M : matrix m n α) :
(⇑(matrix.reindex eₘ eₙ) M)ᴴ = ⇑(matrix.reindex eₙ eₘ) Mᴴ
source
@[simp]
theorem matrix.minor_mul_transpose_minor {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [fintype m] [semiring α] (e : n ≃ m) (M : matrix n m α) :
M.minor id ⇑e ⬝ Mᵀ.minor ⇑e id = M ⬝ Mᵀ
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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.

source
@[simp]
theorem matrix.col_add {m : Type u_2} {α : Type v} [has_add α] (v w : m → α) :
matrix.col (v + w) = matrix.col v + matrix.col w
source
@[simp]
theorem matrix.col_smul {m : Type u_2} {R : Type u_7} {α : Type v} [has_scalar R α] (x : R) (v : m → α) :
matrix.col (x • v) = x • matrix.col v
source
@[simp]
theorem matrix.row_add {m : Type u_2} {α : Type v} [has_add α] (v w : m → α) :
matrix.row (v + w) = matrix.row v + matrix.row w
source
@[simp]
theorem matrix.row_smul {m : Type u_2} {R : Type u_7} {α : Type v} [has_scalar R α] (x : R) (v : m → α) :
matrix.row (x • v) = x • matrix.row v
source
@[simp]
theorem matrix.col_apply {m : Type u_2} {α : Type v} (v : m → α) (i : m) (j : unit) :
matrix.col v i j = v i
source
@[simp]
theorem matrix.row_apply {m : Type u_2} {α : Type v} (v : m → α) (i : unit) (j : m) :
matrix.row v i j = v j
source
@[simp]
theorem matrix.transpose_col {m : Type u_2} {α : Type v} (v : m → α) :
(matrix.col v)ᵀ = matrix.row v
source
@[simp]
theorem matrix.transpose_row {m : Type u_2} {α : Type v} (v : m → α) :
(matrix.row v)ᵀ = matrix.col v
source
@[simp]
theorem matrix.conj_transpose_col {m : Type u_2} {α : Type v} [has_star α] (v : m → α) :
(matrix.col v)ᴴ = matrix.row (star v)
source
@[simp]
theorem matrix.conj_transpose_row {m : Type u_2} {α : Type v} [has_star α] (v : m → α) :
(matrix.row v)ᴴ = matrix.col (star v)
source
theorem matrix.row_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [semiring α] (M : matrix m n α) (v : m → α) :
matrix.row (matrix.vec_mul v M) = matrix.row v ⬝ M
source
theorem matrix.col_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [semiring α] (M : matrix m n α) (v : m → α) :
matrix.col (matrix.vec_mul v M) = (matrix.row v ⬝ M)ᵀ
source
theorem matrix.col_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [semiring α] (M : matrix m n α) (v : n → α) :
matrix.col (M.mul_vec v) = M ⬝ matrix.col v
source
theorem matrix.row_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [semiring α] (M : matrix m n α) (v : n → α) :
matrix.row (M.mul_vec v) = (M ⬝ matrix.col v)ᵀ
source
@[simp]
theorem matrix.row_mul_col_apply {m : Type u_2} {α : Type v} [fintype m] [has_mul α] [add_comm_monoid α] (v w : m → α) (i j : unit) :
(matrix.row v ⬝ matrix.col w) i j = v ⬝ᵥ w
source
def matrix.update_row {m : Type u_2} {n : Type u_3} {α : Type v} [decidable_eq n] (M : matrix n m α) (i : n) (b : m → α) :
matrix n m α

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

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

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

Equations
source
@[simp]
theorem matrix.update_row_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {b : m → α} [decidable_eq n] :
M.update_row i b i = b
source
@[simp]
theorem matrix.update_column_self {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {j : m} {c : n → α} [decidable_eq m] :
M.update_column j c i j = c i
source
@[simp]
theorem matrix.update_row_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {b : m → α} [decidable_eq n] {i' : n} (i_ne : i' ≠ i) :
M.update_row i b i' = M i'
source
@[simp]
theorem matrix.update_column_ne {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {j : m} {c : n → α} [decidable_eq m] {j' : m} (j_ne : j' ≠ j) :
M.update_column j c i j' = M i j'
source
theorem matrix.update_row_apply {m : Type u_2} {n : Type u_3} {α : 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)
source
theorem matrix.update_column_apply {m : Type u_2} {n : Type u_3} {α : 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')
source
@[simp]
theorem matrix.update_column_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_7} [subsingleton m] (A : matrix n m R) (i : m) (b : n → R) :
A.update_column i b = (matrix.col b).minor id (function.const m ())
source
@[simp]
theorem matrix.update_row_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_7} [subsingleton n] (A : matrix n m R) (i : n) (b : m → R) :
A.update_row i b = (matrix.row b).minor (function.const n ()) id
source
theorem matrix.map_update_row {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : matrix n m α} {i : n} {b : m → α} [decidable_eq n] (f : α → β) :
(M.update_row i b).map f = (M.map f).update_row i (f ∘ b)
source
theorem matrix.map_update_column {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : matrix n m α} {j : m} {c : n → α} [decidable_eq m] (f : α → β) :
(M.update_column j c).map f = (M.map f).update_column j (f ∘ c)
source
theorem matrix.update_row_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {j : m} {c : n → α} [decidable_eq m] :
Mᵀ.update_row j c = (M.update_column j c)ᵀ
source
theorem matrix.update_column_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {b : m → α} [decidable_eq n] :
Mᵀ.update_column i b = (M.update_row i b)ᵀ
source
theorem matrix.update_row_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {j : m} {c : n → α} [decidable_eq m] [has_star α] :
Mᴴ.update_row j (star c) = (M.update_column j c)ᴴ
source
theorem matrix.update_column_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix n m α} {i : n} {b : m → α} [decidable_eq n] [has_star α] :
Mᴴ.update_column i (star b) = (M.update_row i b)ᴴ
source
@[simp]
theorem matrix.update_row_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [decidable_eq m] (A : matrix m n α) {i : m} :
A.update_row i (A i) = A
source
@[simp]
theorem matrix.update_column_eq_self {m : Type u_2} {n : Type u_3} {α : Type v} [decidable_eq n] (A : matrix m n α) {i : n} :
A.update_column i (λ (j : m), A j i) = A
source
theorem ring_hom.map_matrix_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [fintype n] [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
source
theorem ring_hom.map_dot_product {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [semiring R] [semiring S] (f : R →+* S) (v w : n → R) :
⇑f (v ⬝ᵥ w) = ⇑f ∘ v ⬝ᵥ ⇑f ∘ w
source
theorem ring_hom.map_vec_mul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [semiring R] [semiring S] (f : R →+* S) (M : matrix n m R) (v : n → R) (i : m) :
⇑f (matrix.vec_mul v M i) = matrix.vec_mul (⇑f ∘ v) (M.map ⇑f) i
source
theorem ring_hom.map_mul_vec {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [semiring R] [semiring S] (f : R →+* S) (M : matrix m n R) (v : n → R) (i : m) :
⇑f (M.mul_vec v i) = (M.map ⇑f).mul_vec (⇑f ∘ v) i