# mathlibdocumentation

data.matrix.basic

# Matrices #

This file defines basic properties of matrices.

Matrices with rows indexed by `m`, columns indexed by `n`, and entries of type `α` are represented with `matrix m n α`. For the typical approach of counting rows and columns, `matrix (fin m) (fin n) α` can be used.

## Notation #

The locale `matrix` gives the following notation:

• `⬝ᵥ` for `matrix.dot_product`
• `⬝` for `matrix.mul`
• `ᵀ` for `matrix.transpose`
• `ᴴ` for `matrix.conj_transpose`

## Implementation notes #

For convenience, `matrix m n α` is defined as `m → n → α`, as this allows elements of the matrix to be accessed with `A i j`. However, it is not advisable to construct matrices using terms of the form `λ i j, _` or even `(λ i j, _ : matrix m n α)`, as these are not recognized by lean as having the right type. Instead, `matrix.of` should be used.

## TODO #

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

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

`matrix m n R` is the type of matrices with entries in `R`, whose rows are indexed by `m` and whose columns are indexed by `n`.

Equations
• n α = (m → n → α)
Instances for `matrix`
theorem matrix.ext_iff {m : Type u_2} {n : Type u_3} {α : 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} {α : Type v} {M N : n α} :
(∀ (i : m) (j : n), M i j = N i j)M = N
def matrix.of {m : Type u_2} {n : Type u_3} {α : Type v} :
(m → n → α) n α

Cast a function into a matrix.

The two sides of the equivalence are definitionally equal types. We want to use an explicit cast to distinguish the types because `matrix` has different instances to pi types (such as `pi.has_mul`, which performs elementwise multiplication, vs `matrix.has_mul`).

If you are defining a matrix, in terms of its entries, either use `of (λ i j, _)`, or use pattern matching in a definition as `| i j := _` (which can only be unfolded when fully-applied). The purpose of this approach is to ensure that terms of the form `(λ i j, _) * (λ i j, _)` do not appear, as the type of `*` can be misleading.

Equations
@[simp]
theorem matrix.of_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) (i : m) (j : n) :
i j = f i j
@[simp]
theorem matrix.of_symm_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : n α) (i : m) (j : n) :
(matrix.of.symm) f i j = f i j
def matrix.map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : n α) (f : α → β) :
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:

• `add_monoid_hom.map_matrix`
• `linear_map.map_matrix`
• `ring_hom.map_matrix`
• `alg_hom.map_matrix`
• `equiv.map_matrix`
• `add_equiv.map_matrix`
• `linear_equiv.map_matrix`
• `ring_equiv.map_matrix`
• `alg_equiv.map_matrix`
Equations
@[simp]
theorem matrix.map_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : n α} {f : α → β} {i : m} {j : n} :
M.map f i j = f (M i j)
@[simp]
theorem matrix.map_id {m : Type u_2} {n : Type u_3} {α : Type v} (M : n α) :
M.map id = M
@[simp]
theorem matrix.map_map {m : Type u_2} {n : Type u_3} {α : Type v} {M : n α} {β : Type u_1} {γ : Type u_4} {f : α → β} {g : β → γ} :
(M.map f).map g = M.map (g f)
theorem matrix.map_injective {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} (hf : function.injective f) :
function.injective (λ (M : n α), M.map f)
def matrix.transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : n α) :
m α

The transpose of a matrix.

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

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

Equations
def matrix.col {m : Type u_2} {α : 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} {α : Type v} (v : n → α) :
α

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

Equations
• x y = v y
@[protected, instance]
def matrix.inhabited {m : Type u_2} {n : Type u_3} {α : Type v} [inhabited α] :
inhabited (matrix m n α)
Equations
@[protected, instance]
def matrix.has_add {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
Equations
@[protected, instance]
def matrix.add_semigroup {m : Type u_2} {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.add_comm_semigroup {m : Type u_2} {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.has_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
has_zero (matrix m n α)
Equations
@[protected, instance]
def matrix.add_zero_class {m : Type u_2} {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.add_monoid {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] :
Equations
@[protected, instance]
def matrix.add_comm_monoid {m : Type u_2} {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.has_neg {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] :
has_neg (matrix m n α)
Equations
@[protected, instance]
def matrix.has_sub {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] :
has_sub (matrix m n α)
Equations
@[protected, instance]
def matrix.add_group {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] :
Equations
@[protected, instance]
def matrix.add_comm_group {m : Type u_2} {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.unique {m : Type u_2} {n : Type u_3} {α : Type v} [unique α] :
unique (matrix m n α)
Equations
@[protected, instance]
def matrix.subsingleton {m : Type u_2} {n : Type u_3} {α : Type v} [subsingleton α] :
@[protected, instance]
def matrix.nontrivial {m : Type u_2} {n : Type u_3} {α : Type v} [nonempty m] [nonempty n] [nontrivial α] :
@[protected, instance]
def matrix.has_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] :
(matrix m n α)
Equations
@[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} [ α] [ α] [ α] :
(matrix m n α)
@[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} [ S] [ α] [ α] [ α] :
(matrix m n α)
@[protected, instance]
def matrix.is_central_scalar {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] [ α] [ α] :
(matrix m n α)
@[protected, instance]
def matrix.mul_action {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [monoid R] [ α] :
(matrix m n α)
Equations
@[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 α] [ α] :
(matrix m n α)
Equations
@[protected, instance]
def matrix.module {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [ α] :
(matrix m n α)
Equations

simp-normal form pulls `of` to the outside.

@[simp]
theorem matrix.of_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
= 0
@[simp]
theorem matrix.of_add_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] (f g : m → n → α) :
@[simp]
theorem matrix.of_sub_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] (f g : m → n → α) :
@[simp]
theorem matrix.neg_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] (f : m → n → α) :
@[simp]
theorem matrix.smul_of {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] (r : R) (f : m → n → α) :
@[protected, 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
@[protected]
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 : n α) :
(M + N).map f = M.map f + N.map f
@[protected]
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 : n α) :
(M - N).map f = M.map f - N.map f
theorem matrix.map_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [ α] [ β] (f : α → β) (r : R) (hf : ∀ (a : α), f (r a) = r f a) (M : n α) :
(r M).map f = r M.map f
theorem matrix.map_smul' {n : Type u_3} {α : Type v} {β : Type w} [has_mul α] [has_mul β] (f : α → β) (r : α) (A : n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) :
(r A).map f = f r A.map f

The scalar action via `has_mul.to_has_smul` is transformed by the same map as the elements of the matrix, when `f` preserves multiplication.

theorem matrix.map_op_smul' {n : Type u_3} {α : Type v} {β : Type w} [has_mul α] [has_mul β] (f : α → β) (r : α) (A : n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) :
A).map f = mul_opposite.op (f r) A.map f

The scalar action via `has_mul.to_has_opposite_smul` is transformed by the same map as the elements of the matrix, when `f` preserves multiplication.

theorem is_smul_regular.matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [ S] {k : R} (hk : k) :
theorem is_left_regular.matrix {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] {k : α} (hk : is_left_regular k) :
@[protected, instance]
def matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : Type v} [is_empty m] :
@[protected, instance]
def matrix.subsingleton_of_empty_right {m : Type u_2} {n : Type u_3} {α : Type v} [is_empty n] :
def matrix.diagonal {n : Type u_3} {α : 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`.

Note that bundled versions exist as:

• `matrix.diagonal_add_monoid_hom`
• `matrix.diagonal_linear_map`
• `matrix.diagonal_ring_hom`
• `matrix.diagonal_alg_hom`
Equations
• j = ite (i = j) (d i) 0
@[simp]
theorem matrix.diagonal_apply_eq {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (d : n → α) (i : n) :
i = d i
@[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) :
j = 0
theorem matrix.diagonal_apply_ne' {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (d : n → α) {i j : n} (h : j i) :
j = 0
@[simp]
theorem matrix.diagonal_eq_diagonal_iff {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] {d₁ d₂ : n → α} :
∀ (i : n), d₁ i = d₂ i
theorem matrix.diagonal_injective {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] :
@[simp]
theorem matrix.diagonal_zero {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] :
matrix.diagonal (λ (_x : n), 0) = 0
@[simp]
theorem matrix.diagonal_transpose {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (v : n → α) :
@[simp]
theorem matrix.diagonal_add {n : Type u_3} {α : Type v} [decidable_eq n] (d₁ d₂ : n → α) :
= matrix.diagonal (λ (i : n), d₁ i + d₂ i)
@[simp]
theorem matrix.diagonal_smul {n : Type u_3} {R : Type u_7} {α : Type v} [decidable_eq n] [monoid R] [add_monoid α] [ α] (r : R) (d : n → α) :
def matrix.diagonal_add_monoid_hom (n : Type u_3) (α : Type v) [decidable_eq n]  :
(n → α) →+ n α

`matrix.diagonal` as an `add_monoid_hom`.

Equations
@[simp]
theorem matrix.diagonal_add_monoid_hom_apply (n : Type u_3) (α : Type v) [decidable_eq n] (d : n → α) :
def matrix.diagonal_linear_map (n : Type u_3) (R : Type u_7) (α : Type v) [decidable_eq n] [semiring R] [ α] :
(n → α) →ₗ[R] n α

`matrix.diagonal` as a `linear_map`.

Equations
@[simp]
theorem matrix.diagonal_linear_map_apply (n : Type u_3) (R : Type u_7) (α : Type v) [decidable_eq n] [semiring R] [ α] (ᾰ : n → α) :
α) =
@[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 → α} :
.map f = matrix.diagonal (λ (m : n), f (d m))
@[simp]
theorem matrix.diagonal_conj_transpose {n : Type u_3} {α : Type v} [decidable_eq n] [add_monoid α] (v : n → α) :
@[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
@[simp]
theorem matrix.diagonal_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
matrix.diagonal (λ (_x : n), 1) = 1
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
@[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
@[simp]
theorem matrix.one_apply_ne {n : Type u_3} {α : 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} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] {i j : n} :
j i1 i j = 0
@[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
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 = 1 j
@[simp]
theorem matrix.bit0_apply {m : Type u_2} {α : 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} {α : Type v} [decidable_eq n] [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} {α : Type v} [decidable_eq n] [has_one α] (M : n α) (i : n) :
bit1 M i i = bit1 (M i i)
@[simp]
theorem matrix.bit1_apply_ne {n : Type u_3} {α : Type v} [decidable_eq n] [has_one α] (M : n α) {i j : n} (h : i j) :
bit1 M i j = bit0 (M i j)
@[simp]
def matrix.diag {n : Type u_3} {α : Type v} (A : n α) (i : n) :
α

The diagonal of a square matrix.

Equations
@[simp]
theorem matrix.diag_diagonal {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (a : n → α) :
.diag = a
@[simp]
theorem matrix.diag_transpose {n : Type u_3} {α : Type v} (A : n α) :
@[simp]
theorem matrix.diag_zero {n : Type u_3} {α : Type v} [has_zero α] :
0.diag = 0
@[simp]
theorem matrix.diag_add {n : Type u_3} {α : Type v} [has_add α] (A B : n α) :
(A + B).diag = A.diag + B.diag
@[simp]
theorem matrix.diag_sub {n : Type u_3} {α : Type v} [has_sub α] (A B : n α) :
(A - B).diag = A.diag - B.diag
@[simp]
theorem matrix.diag_neg {n : Type u_3} {α : Type v} [has_neg α] (A : n α) :
(-A).diag = -A.diag
@[simp]
theorem matrix.diag_smul {n : Type u_3} {R : Type u_7} {α : Type v} [ α] (r : R) (A : n α) :
(r A).diag = r A.diag
@[simp]
theorem matrix.diag_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
1.diag = 1
def matrix.diag_add_monoid_hom (n : Type u_3) (α : Type v)  :
n α →+ n → α

`matrix.diag` as an `add_monoid_hom`.

Equations
@[simp]
theorem matrix.diag_add_monoid_hom_apply (n : Type u_3) (α : Type v) (A : n α) (i : n) :
A i = A.diag i
@[simp]
theorem matrix.diag_linear_map_apply (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [ α] (ᾰ : n α) (ᾰ_1 : n) :
α) ᾰ_1 = ᾰ_1
def matrix.diag_linear_map (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [ α] :
n α →ₗ[R] n → α

`matrix.diag` as a `linear_map`.

Equations
theorem matrix.diag_map {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : n α} :
(A.map f).diag = f A.diag
@[simp]
theorem matrix.diag_conj_transpose {n : Type u_3} {α : Type v} [add_monoid α] (A : n α) :
@[simp]
theorem matrix.diag_list_sum {n : Type u_3} {α : Type v} [add_monoid α] (l : list (matrix n n α)) :
@[simp]
theorem matrix.diag_multiset_sum {n : Type u_3} {α : Type v} (s : multiset (matrix n n α)) :
@[simp]
theorem matrix.diag_sum {n : Type u_3} {α : Type v} {ι : Type u_1} (s : finset ι) (f : ι → n α) :
(s.sum (λ (i : ι), f i)).diag = s.sum (λ (i : ι), (f i).diag)
def matrix.dot_product {m : Type u_2} {α : Type v} [fintype m] [has_mul α] (v w : m → α) :
α

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

Equations
theorem matrix.dot_product_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] (u : m → α) (w : n → α) (v : 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} {α : Type v} [fintype m] (v w : m → α) :
@[simp]
theorem matrix.dot_product_punit {α : Type v} [has_mul α] (v w : punit → α) :
= v punit.star * w punit.star
@[simp]
theorem matrix.dot_product_zero {m : Type u_2} {α : Type v} [fintype m] (v : m → α) :
= 0
@[simp]
theorem matrix.dot_product_zero' {m : Type u_2} {α : Type v} [fintype m] (v : m → α) :
(λ (_x : m), 0) = 0
@[simp]
theorem matrix.zero_dot_product {m : Type u_2} {α : Type v} [fintype m] (v : m → α) :
= 0
@[simp]
theorem matrix.zero_dot_product' {m : Type u_2} {α : Type v} [fintype m] (v : m → α) :
matrix.dot_product (λ (_x : m), 0) v = 0
@[simp]
theorem matrix.add_dot_product {m : Type u_2} {α : Type v} [fintype m] (u v w : m → α) :
@[simp]
theorem matrix.dot_product_add {m : Type u_2} {α : Type v} [fintype m] (u v w : m → α) :
(v + w) =
@[simp]
theorem matrix.sum_elim_dot_product_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] (u v : m → α) (x y : n → α) :
(sum.elim v y) =
@[simp]
theorem matrix.diagonal_dot_product {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v w : m → α) (i : m) :
= v i * w i
@[simp]
theorem matrix.dot_product_diagonal {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v w : m → α) (i : m) :
= v i * w i
@[simp]
theorem matrix.dot_product_diagonal' {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v w : m → α) (i : m) :
(λ (j : m), i) = v i * w i
@[simp]
theorem matrix.single_dot_product {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v : m → α) (x : α) (i : m) :
v = x * v i
@[simp]
theorem matrix.dot_product_single {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v : m → α) (x : α) (i : m) :
x) = v i * x
@[simp]
theorem matrix.neg_dot_product {m : Type u_2} {α : Type v} [fintype m] (v w : m → α) :
w =
@[simp]
theorem matrix.dot_product_neg {m : Type u_2} {α : Type v} [fintype m] (v w : m → α) :
(-w) =
@[simp]
theorem matrix.sub_dot_product {m : Type u_2} {α : Type v} [fintype m] (u v w : m → α) :
@[simp]
theorem matrix.dot_product_sub {m : Type u_2} {α : Type v} [fintype m] (u v w : m → α) :
(v - w) =
@[simp]
theorem matrix.smul_dot_product {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [monoid R] [has_mul α] [ α] [ α] (x : R) (v w : m → α) :
@[simp]
theorem matrix.dot_product_smul {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [monoid R] [has_mul α] [ α] [ α] (x : R) (v w : m → α) :
(x w) = x
theorem matrix.star_dot_product_star {m : Type u_2} {α : Type v} [fintype m] [star_ring α] (v w : m → α) :
theorem matrix.star_dot_product {m : Type u_2} {α : Type v} [fintype m] [star_ring α] (v w : m → α) :
theorem matrix.dot_product_star {m : Type u_2} {α : Type v} [fintype m] [star_ring α] (v w : m → α) :
@[protected]
def matrix.mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [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 `N`. This is currently only defined when `m` is finite.

Equations
theorem matrix.mul_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [has_mul α] {M : m α} {N : n α} {i : l} {k : n} :
M.mul N i k = finset.univ.sum (λ (j : m), M i j * N j k)
@[protected, instance]
def matrix.has_mul {n : Type u_3} {α : Type v} [fintype n] [has_mul α]  :
has_mul (matrix n n α)
Equations
@[simp]
theorem matrix.mul_eq_mul {n : Type u_3} {α : Type v} [fintype n] [has_mul α] (M N : n α) :
M * N = M.mul N
theorem matrix.mul_apply' {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [has_mul α] {M : m α} {N : n α} {i : l} {k : n} :
M.mul N i k = matrix.dot_product (λ (j : m), M i j) (λ (j : m), N j k)
@[simp]
theorem matrix.diagonal_neg {n : Type u_3} {α : Type v} [decidable_eq n] [add_group α] (d : n → α) :
= matrix.diagonal (λ (i : n), -d i)
theorem matrix.sum_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (i : m) (j : n) (s : finset β) (g : β → n α) :
s.sum (λ (c : β), g c) i j = s.sum (λ (c : β), g c i j)
@[simp]
theorem matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_mul α] [fintype n] [monoid R] [ α] [ α] (a : R) (M : n α) (N : l α) :
(a M).mul N = a M.mul N
@[simp]
theorem matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_mul α] [fintype n] [monoid R] [ α] [ α] (M : n α) (a : R) (N : l α) :
M.mul (a N) = a M.mul N
@[protected, simp]
theorem matrix.mul_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M : n α) :
M.mul 0 = 0
@[protected, simp]
theorem matrix.zero_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (M : n α) :
0.mul M = 0
@[protected]
theorem matrix.mul_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (L : n α) (M N : o α) :
L.mul (M + N) = L.mul M + L.mul N
@[protected]
theorem matrix.add_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (L M : m α) (N : n α) :
(L + M).mul N = L.mul N + M.mul N
@[protected, instance]
def matrix.non_unital_non_assoc_semiring {n : Type u_3} {α : Type v} [fintype n] :
Equations
@[simp]
theorem matrix.diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [decidable_eq m] (d : m → α) (M : n α) (i : m) (j : n) :
.mul M i j = d i * M i j
@[simp]
theorem matrix.mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (d : n → α) (M : n α) (i : m) (j : n) :
M.mul i j = M i j * d j
@[simp]
theorem matrix.diagonal_mul_diagonal {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (d₁ d₂ : n → α) :
(matrix.diagonal d₁).mul (matrix.diagonal d₂) = matrix.diagonal (λ (i : n), d₁ i * d₂ i)
theorem matrix.diagonal_mul_diagonal' {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (d₁ d₂ : n → α) :
= matrix.diagonal (λ (i : n), d₁ i * d₂ i)
theorem matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [decidable_eq m] (M : n α) (a : α) :
a M = (matrix.diagonal (λ (_x : m), a)).mul M
@[simp]
theorem matrix.diag_col_mul_row {n : Type u_3} {α : Type v} (a b : n → α) :
def matrix.add_monoid_hom_mul_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (M : m α) :
n α →+ n α

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

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

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

Equations
@[protected]
theorem matrix.sum_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [fintype m] (s : finset β) (f : β → m α) (M : n α) :
(s.sum (λ (a : β), f a)).mul M = s.sum (λ (a : β), (f a).mul M)
@[protected]
theorem matrix.mul_sum {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [fintype m] (s : finset β) (f : β → n α) (M : m α) :
M.mul (s.sum (λ (a : β), f a)) = s.sum (λ (a : β), M.mul (f a))
@[protected, instance]
def matrix.semiring.is_scalar_tower {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [monoid R] [ α] [ α] :
(matrix n n α) (matrix n n α)

This instance enables use with `smul_mul_assoc`.

@[protected, instance]
def matrix.semiring.smul_comm_class {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [monoid R] [ α] [ α] :
(matrix n n α) (matrix n n α)

This instance enables use with `mul_smul_comm`.

@[protected, simp]
theorem matrix.one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [decidable_eq m] (M : n α) :
1.mul M = M
@[protected, simp]
theorem matrix.mul_one {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (M : n α) :
M.mul 1 = M
@[protected, instance]
def matrix.non_assoc_semiring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] :
Equations
@[simp]
theorem matrix.map_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [fintype n] {L : n α} {M : o α} {f : α →+* β} :
(L.mul M).map f = (L.map f).mul (M.map f)
def matrix.diagonal_ring_hom (n : Type u_3) (α : Type v) [fintype n] [decidable_eq n] :
(n → α) →+* n α

`matrix.diagonal` as a `ring_hom`.

Equations
@[simp]
theorem matrix.diagonal_ring_hom_apply (n : Type u_3) (α : Type v) [fintype n] [decidable_eq n] (d : n → α) :
@[protected]
theorem matrix.mul_assoc {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype m] [fintype n] (L : m α) (M : n α) (N : o α) :
(L.mul M).mul N = L.mul (M.mul N)
@[protected, instance]
def matrix.non_unital_semiring {n : Type u_3} {α : Type v} [fintype n] :
Equations
@[protected, instance]
def matrix.semiring {n : Type u_3} {α : Type v} [semiring α] [fintype n] [decidable_eq n] :
semiring (matrix n n α)
Equations
@[protected, simp]
theorem matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M : n α) (N : o α) :
(-M).mul N = -M.mul N
@[protected, simp]
theorem matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M : n α) (N : o α) :
M.mul (-N) = -M.mul N
@[protected]
theorem matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M M' : n α) (N : o α) :
(M - M').mul N = M.mul N - M'.mul N
@[protected]
theorem matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M : n α) (N N' : o α) :
M.mul (N - N') = M.mul N - M.mul N'
@[protected, instance]
def matrix.non_unital_non_assoc_ring {n : Type u_3} {α : Type v} [fintype n] :
Equations
@[protected, instance]
def matrix.non_unital_ring {n : Type u_3} {α : Type v} [fintype n]  :
Equations
@[protected, instance]
def matrix.non_assoc_ring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n]  :
Equations
@[protected, instance]
def matrix.ring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] [ring α] :
ring (matrix n n α)
Equations
theorem matrix.diagonal_pow {n : Type u_3} {α : Type v} [semiring α] [fintype n] [decidable_eq n] (v : n → α) (k : ) :
@[simp]
theorem matrix.mul_mul_left {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [semiring α] [fintype n] (M : n α) (N : o α) (a : α) :
(matrix.of (λ (i : m) (j : n), a * M i j)).mul N = a M.mul 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} {α : Type v} [semiring α] [decidable_eq n] [fintype n] :
= λ (a : α), a 1
theorem matrix.scalar_apply_eq {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] (a : α) (i : n) :
a i i = a
theorem matrix.scalar_apply_ne {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] (a : α) (i j : n) (h : i j) :
a i j = 0
theorem matrix.scalar_inj {n : Type u_3} {α : Type v} [semiring α] [decidable_eq n] [fintype n] [nonempty n] {r s : α} :
r = s r = s
theorem matrix.smul_eq_mul_diagonal {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (M : n α) (a : α) :
a M = M.mul (matrix.diagonal (λ (_x : n), a))
@[simp]
theorem matrix.mul_mul_right {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] (M : n α) (N : o α) (a : α) :
M.mul (matrix.of (λ (i : n) (j : o), a * N i j)) = a M.mul N
theorem matrix.scalar.commute {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] (r : α) (M : n α) :
commute ( r) M
@[protected, instance]
def matrix.algebra {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] :
(matrix n n α)
Equations
theorem matrix.algebra_map_matrix_apply {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] {r : R} {i j : n} :
(matrix n n α)) r i j = ite (i = j) ( α) r) 0
theorem matrix.algebra_map_eq_diagonal {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] (r : R) :
(matrix n n α)) r = matrix.diagonal ( (n → α)) r)
@[simp]
theorem matrix.algebra_map_eq_smul {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] (r : R) :
(matrix n n R)) r = r 1
theorem matrix.algebra_map_eq_diagonal_ring_hom {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] :
(matrix n n α) = .comp (n → α))
@[simp]
theorem matrix.map_algebra_map {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [fintype n] [decidable_eq n] [semiring α] [semiring β] [ α] [ β] (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f ( α) r) = β) r) :
( (matrix n n α)) r).map f = (matrix n n β)) r
def matrix.diagonal_alg_hom {n : Type u_3} (R : Type u_7) {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] :
(n → α) →ₐ[R] n α

`matrix.diagonal` as an `alg_hom`.

Equations
@[simp]
theorem matrix.diagonal_alg_hom_apply {n : Type u_3} (R : Type u_7) {α : Type v} [fintype n] [decidable_eq n] [semiring α] [ α] (d : n → α) :

### Bundled versions of `matrix.map`#

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

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

Equations
@[simp]
theorem equiv.map_matrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α β) (M : n α) :
@[simp]
theorem equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} :
@[simp]
theorem equiv.map_matrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α β) :
@[simp]
theorem equiv.map_matrix_trans {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} (f : α β) (g : β γ) :
def add_monoid_hom.map_matrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α →+ β) :
n α →+ 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
@[simp]
theorem add_monoid_hom.map_matrix_apply {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α →+ β) (M : n α) :
@[simp]
theorem add_monoid_hom.map_matrix_id {m : Type u_2} {n : Type u_3} {α : Type v}  :
@[simp]
theorem add_monoid_hom.map_matrix_comp {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {γ : Type u_9} (f : β →+ γ) (g : α →+ β) :
def add_equiv.map_matrix {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α ≃+ β) :
n α ≃+ 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
@[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 : n α) :
@[simp]
theorem add_equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] :
@[simp]
theorem add_equiv.map_matrix_symm {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_add α] [has_add β] (f : α ≃+ β) :
@[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 : β ≃+ γ) :
def linear_map.map_matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [ α] [ β] (f : α →ₗ[R] β) :
n α →ₗ[R] 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
@[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] [ α] [ β] (f : α →ₗ[R] β) (M : n α) :
@[simp]
theorem linear_map.map_matrix_id {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [ α] :
@[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] [ α] [ β] [ γ] (f : β →ₗ[R] γ) (g : α →ₗ[R] β) :
def linear_equiv.map_matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [semiring R] [ α] [ β] (f : α ≃ₗ[R] β) :
n α ≃ₗ[R] 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
@[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] [ α] [ β] (f : α ≃ₗ[R] β) (M : n α) :
@[simp]
theorem linear_equiv.map_matrix_refl {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [ α] :
α).map_matrix = (matrix m n α)
@[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] [ α] [ β] (f : α ≃ₗ[R] β) :
@[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] [ α] [ β] [ γ] (f : α ≃ₗ[R] β) (g : β ≃ₗ[R] γ) :
def ring_hom.map_matrix {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] (f : α →+* β) :
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
@[simp]
theorem ring_hom.map_matrix_apply {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] (f : α →+* β) (M : m α) :
@[simp]
theorem ring_hom.map_matrix_id {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m]  :
= ring_hom.id (matrix m m α)
@[simp]
theorem ring_hom.map_matrix_comp {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] (f : β →+* γ) (g : α →+* β) :
def ring_equiv.map_matrix {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] (f : α ≃+* β) :
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
@[simp]
theorem ring_equiv.map_matrix_apply {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] (f : α ≃+* β) (M : m α) :
@[simp]
theorem ring_equiv.map_matrix_refl {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m]  :
@[simp]
theorem ring_equiv.map_matrix_symm {m : Type u_2} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] (f : α ≃+* β) :
@[simp]
theorem ring_equiv.map_matrix_trans {m : Type u_2} {α : Type v} {β : Type w} {γ : Type u_9} [fintype m] [decidable_eq m] (f : α ≃+* β) (g : β ≃+* γ) :
def alg_hom.map_matrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [semiring α] [semiring β] [ α] [ β] (f : α →ₐ[R] β) :
m α →ₐ[R] 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
@[simp]
theorem alg_hom.map_matrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [semiring α] [semiring β] [ α] [ β] (f : α →ₐ[R] β) (M : m α) :
@[simp]
theorem alg_hom.map_matrix_id {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [decidable_eq m] [semiring α] [ α] :
α).map_matrix = (matrix m m α)
@[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] [semiring α] [semiring β] [semiring γ] [ α] [ β] [ γ] (f : β →ₐ[R] γ) (g : α →ₐ[R] β) :
@[simp]
theorem alg_equiv.map_matrix_apply {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [semiring α] [semiring β] [ α] [ β] (f : α ≃ₐ[R] β) (M : m α) :
def alg_equiv.map_matrix {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [semiring α] [semiring β] [ α] [ β] (f : α ≃ₐ[R] β) :
m α ≃ₐ[R] 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
@[simp]
theorem alg_equiv.map_matrix_refl {m : Type u_2} {R : Type u_7} {α : Type v} [fintype m] [decidable_eq m] [semiring α] [ α] :
@[simp]
theorem alg_equiv.map_matrix_symm {m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [fintype m] [decidable_eq m] [semiring α] [semiring β] [ α] [ β] (f : α ≃ₐ[R] β) :
@[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] [semiring α] [semiring β] [semiring γ] [ α] [ β] [ γ] (f : α ≃ₐ[R] β) (g : β ≃ₐ[R] γ) :
def matrix.vec_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] (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
theorem matrix.vec_mul_vec_eq {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] (w : m → α) (v : n → α) :
def matrix.mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (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} {α : Type v} [fintype m] (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)
def matrix.mul_vec.add_monoid_hom_left {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (v : n → α) :
n α →+ m → α

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

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

Associate the dot product of `mul_vec` to the left.

@[simp]
theorem matrix.mul_vec_zero {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A : n α) :
A.mul_vec 0 = 0
@[simp]
theorem matrix.zero_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (A : n α) :
= 0
@[simp]
theorem matrix.zero_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (v : n → α) :
0.mul_vec v = 0
@[simp]
theorem matrix.vec_mul_zero {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (v : m → α) :
= 0
theorem matrix.smul_mul_vec_assoc {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [fintype n] [monoid R] [ α] [ α] (a : R) (A : n α) (b : n → α) :
(a A).mul_vec b = a A.mul_vec b
theorem matrix.mul_vec_add {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A : n α) (x y : n → α) :
A.mul_vec (x + y) = A.mul_vec x + A.mul_vec y
theorem matrix.add_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A B : n α) (x : n → α) :
(A + B).mul_vec x = A.mul_vec x + B.mul_vec x
theorem matrix.vec_mul_add {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (A B : n α) (x : m → α) :
(A + B) = +
theorem matrix.add_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (A : n α) (x y : m → α) :
matrix.vec_mul (x + y) A = +
theorem matrix.vec_mul_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [monoid R] [ S] [ S] (M : m S) (b : R) (v : n → S) :
matrix.vec_mul (b v) M = b
theorem matrix.mul_vec_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [monoid R] [ S] [ S] (M : n S) (b : R) (v : n → S) :
M.mul_vec (b v) = b M.mul_vec v
@[simp]
theorem matrix.mul_vec_single {m : Type u_2} {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] (M : n R) (j : n) (x : R) :
M.mul_vec x) = λ (i : m), M i j * x
@[simp]
theorem matrix.single_vec_mul {m : Type u_2} {n : Type u_3} {R : Type u_7} [fintype m] [decidable_eq m] (M : n R) (i : m) (x : R) :
matrix.vec_mul x) M = λ (j : n), x * M i j
@[simp]
theorem matrix.diagonal_mul_vec_single {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] (v : n → R) (j : n) (x : R) :
x) = (v j * x)
@[simp]
theorem matrix.single_vec_mul_diagonal {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] (v : n → R) (j : n) (x : R) :
matrix.vec_mul x) = (x * v j)
@[simp]
theorem matrix.vec_mul_vec_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype m] (v : m → α) (M : n α) (N : o α) :
N = (M.mul N)
@[simp]
theorem matrix.mul_vec_mul_vec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] (v : o → α) (M : n α) (N : o α) :
M.mul_vec (N.mul_vec v) = (M.mul N).mul_vec v
theorem matrix.star_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [star_ring α] (M : n α) (v : n → α) :
theorem matrix.star_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [star_ring α] (M : n α) (v : m → α) :
theorem matrix.mul_vec_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [star_ring α] (A : n α) (x : m → α) :
theorem matrix.vec_mul_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [star_ring α] (A : n α) (x : n → α) :
theorem matrix.mul_mul_apply {n : Type u_3} {α : Type v} [fintype n] (A B C : n α) (i j : n) :
(A.mul B).mul C i j = matrix.dot_product (A i) (B.mul_vec (C.transpose j))
@[simp]
theorem matrix.one_mul_vec {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v : m → α) :
1.mul_vec v = v
@[simp]
theorem matrix.vec_mul_one {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (v : m → α) :
= v
theorem matrix.neg_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (v : m → α) (A : n α) :
A = -
theorem matrix.vec_mul_neg {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (v : m → α) (A : n α) :
(-A) = -
theorem matrix.neg_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (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} {α : Type v} [fintype n] (v : n → α) (A : n α) :
A.mul_vec (-v) = -A.mul_vec v
theorem matrix.sub_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A B : n α) (x : n → α) :
(A - B).mul_vec x = A.mul_vec x - B.mul_vec x
theorem matrix.vec_mul_sub {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (A B : n α) (x : m → α) :
(A - B) = -
theorem matrix.mul_vec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] (A : n α) (x : m → α) :
theorem matrix.vec_mul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A : n α) (x : n → α) :
= A.mul_vec x
theorem matrix.mul_vec_vec_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] (A : n α) (B : n α) (x : o → α) :
theorem matrix.vec_mul_mul_vec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype m] [fintype n] (A : n α) (B : o α) (x : n → α) :
theorem matrix.mul_vec_smul_assoc {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (A : n α) (b : n → α) (a : α) :
A.mul_vec (a b) = a A.mul_vec b
@[simp]
theorem matrix.transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} (M : n α) (i : m) (j : n) :
M.transpose 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} {α : Type v} (M : n α) :
@[simp]
theorem matrix.transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
@[simp]
theorem matrix.transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
@[simp]
theorem matrix.transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] (M N : n α) :
(M + N).transpose =
@[simp]
theorem matrix.transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] (M N : n α) :
(M - N).transpose =
@[simp]
theorem matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] (M : n α) (N : l α) :
(M.mul N).transpose =
@[simp]
theorem matrix.transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_1} [ α] (c : R) (M : n α) :
@[simp]
theorem matrix.transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] (M : n α) :
theorem matrix.transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : n α} :
@[simp]
theorem matrix.transpose_add_equiv_apply (m : Type u_2) (n : Type u_3) (α : Type v) [has_add α] (M : n α) :
α) M = M.transpose
def matrix.transpose_add_equiv (m : Type u_2) (n : Type u_3) (α : Type v) [has_add α] :
n α ≃+ m α

`matrix.transpose` as an `add_equiv`

Equations
@[simp]
theorem matrix.transpose_add_equiv_symm (m : Type u_2) (n : Type u_3) (α : Type v) [has_add α] :
α).symm =
theorem matrix.transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] (l : list (matrix m n α)) :
theorem matrix.transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} (s : multiset (matrix m n α)) :
theorem matrix.transpose_sum {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_1} (s : finset ι) (M : ι → n α) :
(s.sum (λ (i : ι), M i)).transpose = s.sum (λ (i : ι), (M i).transpose)
@[simp]
theorem matrix.transpose_linear_equiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [ α] (ᾰ : n α) :
α) = α).to_fun
def matrix.transpose_linear_equiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [ α] :
n α ≃ₗ[R] m α

`matrix.transpose` as a `linear_map`

Equations
@[simp]
theorem matrix.transpose_linear_equiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [ α] :
α).symm =
def matrix.transpose_ring_equiv (m : Type u_2) (α : Type v) [fintype m] :
m α ≃+* (matrix m m α)ᵐᵒᵖ

`matrix.transpose` as a `ring_equiv` to the opposite ring

Equations
@[simp]
theorem matrix.transpose_ring_equiv_apply (m : Type u_2) (α : Type v) [fintype m] (M : m α) :
@[simp]
theorem matrix.transpose_ring_equiv_symm_apply (m : Type u_2) (α : Type v) [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
.symm) M =
@[simp]
theorem matrix.transpose_pow {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (M : m α) (k : ) :
(M ^ k).transpose = M.transpose ^ k
theorem matrix.transpose_list_prod {m : Type u_2} {α : Type v} [fintype m] [decidable_eq m] (l : list (matrix m m α)) :
@[simp]
theorem matrix.transpose_alg_equiv_symm_apply (m : Type u_2) (R : Type u_7) (α : Type v) [fintype m] [decidable_eq m] [ α] (ᾰ : (matrix m m α)ᵐᵒᵖ) :
α).symm) =
@[simp]
theorem matrix.transpose_alg_equiv_apply (m : Type u_2) (R : Type u_7) (α : Type v) [fintype m] [decidable_eq m] [ α] (M : m α) :
α) M =
def matrix.transpose_alg_equiv (m : Type u_2) (R : Type u_7) (α : Type v) [fintype m] [decidable_eq m] [ α] :
m α ≃ₐ[R] (matrix m m α)ᵐᵒᵖ

`matrix.transpose` as an `alg_equiv` to the opposite ring

Equations
@[simp]
theorem matrix.conj_transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} [has_star α] (M : n α) (i : m) (j : n) :
i = has_star.star (M i j)

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

Compare with `mul_apply`, `diagonal_apply_eq`, etc.

@[simp]
theorem matrix.conj_transpose_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : n α) :
@[simp]
theorem matrix.conj_transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α]  :
@[simp]
theorem matrix.conj_transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [semiring α] [star_ring α] :
@[simp]
theorem matrix.conj_transpose_add {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] (M N : n α) :
@[simp]
theorem matrix.conj_transpose_sub {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] (M N : n α) :
@[simp]
theorem matrix.conj_transpose_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_star R] [has_star α] [ α] [ α] (c : R) (M : n α) :

Note that `star_module` is quite a strong requirement; as such we also provide the following variants which this lemma would not apply to:

• `matrix.conj_transpose_smul_non_comm`
• `matrix.conj_transpose_nsmul`
• `matrix.conj_transpose_zsmul`
• `matrix.conj_transpose_nat_cast_smul`
• `matrix.conj_transpose_int_cast_smul`
• `matrix.conj_transpose_inv_nat_cast_smul`
• `matrix.conj_transpose_inv_int_cast_smul`
• `matrix.conj_transpose_rat_smul`
• `matrix.conj_transpose_rat_cast_smul`
@[simp]
theorem matrix.conj_transpose_smul_non_comm {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_star R] [has_star α] [ α] [ α] (c : R) (M : n α) (h : ∀ (r : R) (a : α), has_star.star (r a) = ) :
@[simp]
theorem matrix.conj_transpose_smul_self {m : Type u_2} {n : Type u_3} {α : Type v} [semigroup α] (c : α) (M : n α) :
@[simp]
theorem matrix.conj_transpose_nsmul {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_zsmul {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_nat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_int_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ring R] [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_inv_nat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_inv_int_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_rat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_rat_smul {m : Type u_2} {n : Type u_3} {α : Type v} [ α] (c : ) (M : n α) :
@[simp]
theorem matrix.conj_transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [star_ring α] (M : n α) (N : l α) :
@[simp]
theorem matrix.conj_transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] (M : n α) :
theorem matrix.conj_transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_star α] [has_star β] {A : n α} (f : α → β)  :
@[simp]
theorem matrix.conj_transpose_add_equiv_apply (m : Type u_2) (n : Type u_3) (α : Type v) [add_monoid α] (M : n α) :
def matrix.conj_transpose_add_equiv (m : Type u_2) (n : Type u_3) (α : Type v) [add_monoid α]  :
n α ≃+ m α

`matrix.conj_transpose` as an `add_equiv`

Equations
@[simp]
theorem matrix.conj_transpose_add_equiv_symm (m : Type u_2) (n : Type u_3) (α : Type v) [add_monoid α]  :
theorem matrix.conj_transpose_list_sum {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] (l : list (matrix m n α)) :
theorem matrix.conj_transpose_multiset_sum {m : Type u_2} {n : Type u_3} {α : Type v} (s : multiset (matrix m n α)) :
theorem matrix.conj_transpose_sum {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_1} (s : finset ι) (M : ι → n α) :
(s.sum (λ (i : ι), M i)).conj_transpose = s.sum (λ (i : ι), (M i).conj_transpose)
@[simp]
theorem matrix.conj_transpose_linear_equiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [star_ring R] [ α] [ α] (ᾰ : n α) :
α) =
def matrix.conj_transpose_linear_equiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [star_ring R] [ α] [ α] :
n α ≃ₗ⋆[R] m α

`matrix.conj_transpose` as a `linear_map`

Equations
@[simp]
theorem matrix.conj_transpose_linear_equiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [star_ring R] [ α] [ α] :
α).symm =
def matrix.conj_transpose_ring_equiv (m : Type u_2) (α : Type v) [semiring α] [star_ring α] [fintype m] :
m α ≃+* (matrix m m α)ᵐᵒᵖ

`matrix.conj_transpose` as a `ring_equiv` to the opposite ring

Equations
@[simp]
theorem matrix.conj_transpose_ring_equiv_apply (m : Type u_2) (α : Type v) [semiring α] [star_ring α] [fintype m] (M : m α) :
@[simp]
theorem matrix.conj_transpose_ring_equiv_symm_apply (m : Type u_2) (α : Type v) [semiring α] [star_ring α] [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
@[simp]
theorem matrix.conj_transpose_pow {m : Type u_2} {α : Type v} [semiring α] [star_ring α] [fintype m] [decidable_eq m] (M : m α) (k : ) :
theorem matrix.conj_transpose_list_prod {m : Type u_2} {α : Type v} [semiring α] [star_ring α] [fintype m] [decidable_eq m] (l : list (matrix m m α)) :
@[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
theorem matrix.star_eq_conj_transpose {m : Type u_2} {α : Type v} [has_star α] (M : m α) :
@[simp]
theorem matrix.star_apply {n : Type u_3} {α : Type v} [has_star α] (M : n α) (i j : n) :
j = has_star.star (M j i)
@[protected, instance]
def matrix.has_involutive_star {n : Type u_3} {α : Type v}  :
Equations
@[protected, instance]
def matrix.star_add_monoid {n : Type u_3} {α : Type v} [add_monoid α]  :

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

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

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

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

A version of `star_mul` for `⬝` instead of `*`.

def matrix.submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : n α) (r_reindex : l → m) (c_reindex : o → n) :
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.submatrix r_reindex c_reindex : matrix l o α` is defined by `(M.submatrix 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
@[simp]
theorem matrix.submatrix_apply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : n α) (r_reindex : l → m) (c_reindex : o → n) (i : l) (j : o) :
A.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)
@[simp]
theorem matrix.submatrix_id_id {m : Type u_2} {n : Type u_3} {α : Type v} (A : n α) :
= A
@[simp]
theorem matrix.submatrix_submatrix {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 : n α) (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) :
(A.submatrix r₁ c₁).submatrix r₂ c₂ = A.submatrix (r₁ r₂) (c₁ c₂)
@[simp]
theorem matrix.transpose_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (A : n α) (r_reindex : l → m) (c_reindex : o → n) :
(A.submatrix r_reindex c_reindex).transpose = A.transpose.submatrix c_reindex r_reindex
@[simp]
theorem matrix.conj_transpose_submatrix {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_star α] (A : n α) (r_reindex : l → m) (c_reindex : o → n) :
(A.submatrix r_reindex c_reindex).conj_transpose = A.conj_transpose.submatrix c_reindex r_reindex
theorem matrix.submatrix_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_add α] (A B : n α) :
(A + B).submatrix =
theorem matrix.submatrix_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_neg α] (A : n α) :
theorem matrix.submatrix_sub {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_sub α] (A B : n α) :
(A - B).submatrix =
@[simp]
theorem matrix.submatrix_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [has_zero α] :
theorem matrix.submatrix_smul {l : Type u_1} {m : Type u_2}