mathlib3 documentation

data.matrix.basic

Matrices #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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.

source
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
Instances for matrix
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.of {m : Type u_2} {n : Type u_3} {α : Type v} :
(m → n → α) ≃ matrix m 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, use of (λ i j, _). The purpose of this approach is to ensure that terms of th e form (λ i j, _) * (λ i j, _) do not appear, as the type of * can be misleading.

Porting note: In Lean 3, it is also safe to use pattern matching in a definition as | i j := _, which can only be unfolded when fully-applied. leanprover/lean4#2042 means this does not (currently) work in Lean 4.

Equations
source
@[simp]
theorem matrix.of_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) (i : m) (j : n) :
⇑matrix.of f i j = f i j
source
@[simp]
theorem matrix.of_symm_apply {m : Type u_2} {n : Type u_3} {α : Type v} (f : matrix m n α) (i : m) (j : n) :
⇑(matrix.of.symm) f i j = f i j
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
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
theorem matrix.map_injective {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} (hf : function.injective f) :
function.injective (λ (M : matrix m n α), M.map 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
Instances for matrix.transpose
source
@[simp]
theorem matrix.transpose_apply {m : Type u_2} {n : Type u_3} {α : Type v} (M : matrix m n α) (i : n) (j : m) :
M.transpose i j = M j i
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
@[simp]
theorem matrix.col_apply {m : Type u_2} {α : Type v} (w : m → α) (i : m) (j : unit) :
matrix.col w i j = w i
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
@[simp]
theorem matrix.row_apply {n : Type u_3} {α : Type v} (v : n → α) (i : unit) (j : n) :
matrix.row v i j = v j
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_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_smul R α] :
has_smul 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_smul R α] [has_smul 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_smul R S] [has_smul R α] [has_smul 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_smul R α] [has_smul 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

simp-normal form pulls of to the outside.

source
@[simp]
theorem matrix.of_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
⇑matrix.of 0 = 0
source
@[simp]
theorem matrix.of_add_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_add α] (f g : m → n → α) :
⇑matrix.of f + ⇑matrix.of g = ⇑matrix.of (f + g)
source
@[simp]
theorem matrix.of_sub_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_sub α] (f g : m → n → α) :
⇑matrix.of f - ⇑matrix.of g = ⇑matrix.of (f - g)
source
@[simp]
theorem matrix.neg_of {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] (f : m → n → α) :
-⇑matrix.of f = ⇑matrix.of (-f)
source
@[simp]
theorem matrix.smul_of {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [has_smul R α] (r : R) (f : m → n → α) :
r • ⇑matrix.of f = ⇑matrix.of (r • f)
source
@[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
source
@[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 : matrix m n α) :
(M + N).map f = M.map f + N.map f
source
@[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 : 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_smul R α] [has_smul 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 matrix.map_smul' {n : Type u_3} {α : Type v} {β : Type w} [has_mul α] [has_mul β] (f : α → β) (r : α) (A : matrix n 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.

source
theorem matrix.map_op_smul' {n : Type u_3} {α : Type v} {β : Type w} [has_mul α] [has_mul β] (f : α → β) (r : α) (A : matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) :
(mul_opposite.op r • 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.

source
theorem is_smul_regular.matrix {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [has_smul 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
@[protected, instance]
def matrix.subsingleton_of_empty_left {m : Type u_2} {n : Type u_3} {α : Type v} [is_empty m] :
subsingleton (matrix m n α)
source
@[protected, instance]
def 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
theorem matrix.diagonal_apply {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (d : n → α) (i j : n) :
matrix.diagonal d i j = ite (i = j) (d i) 0
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
@[simp]
theorem matrix.diagonal_eq_diagonal_iff {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] {d₁ d₂ : n → α} :
matrix.diagonal d₁ = matrix.diagonal d₂ ↔ ∀ (i : n), d₁ i = d₂ i
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).transpose = 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] [add_monoid α] [star_add_monoid α] (v : n → α) :
(matrix.diagonal v).conj_transpose = matrix.diagonal (has_star.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_zero_class α] [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_zero_class α] [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_zero_class α] [has_one α] (M : matrix n n α) {i j : n} (h : i ≠ j) :
bit1 M i j = bit0 (M i j)
source
@[simp]
def matrix.diag {n : Type u_3} {α : Type v} (A : matrix n n α) (i : n) :
α

The diagonal of a square matrix.

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

matrix.diag as an add_monoid_hom.

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

matrix.diag as a linear_map.

Equations
source
theorem matrix.diag_map {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : matrix n n α} :
(A.map f).diag = f ∘ A.diag
source
@[simp]
theorem matrix.diag_conj_transpose {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] (A : matrix n n α) :
A.conj_transpose.diag = has_star.star A.diag
source
@[simp]
theorem matrix.diag_list_sum {n : Type u_3} {α : Type v} [add_monoid α] (l : list (matrix n n α)) :
l.sum.diag = (list.map matrix.diag l).sum
source
@[simp]
theorem matrix.diag_multiset_sum {n : Type u_3} {α : Type v} [add_comm_monoid α] (s : multiset (matrix n n α)) :
s.sum.diag = (multiset.map matrix.diag s).sum
source
@[simp]
theorem matrix.diag_sum {n : Type u_3} {α : Type v} {ι : Type u_1} [add_comm_monoid α] (s : finset ι) (f : ι → matrix n n α) :
(s.sum (λ (i : ι), f i)).diag = s.sum (λ (i : ι), (f i).diag)
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 α) :
matrix.dot_product (λ (j : n), matrix.dot_product u (λ (i : m), v i j)) w = matrix.dot_product u (λ (i : m), matrix.dot_product (v i) w)
source
theorem matrix.dot_product_comm {m : Type u_2} {α : Type v} [fintype m] [add_comm_monoid α] [comm_semigroup α] (v w : m → α) :
matrix.dot_product v w = matrix.dot_product w v
source
@[simp]
theorem matrix.dot_product_punit {α : Type v} [add_comm_monoid α] [has_mul α] (v w : punit → α) :
matrix.dot_product v w = v punit.star * w punit.star
source
theorem matrix.dot_product_one {n : Type u_3} {α : Type v} [fintype n] [mul_one_class α] [add_comm_monoid α] (v : n → α) :
matrix.dot_product v 1 = finset.univ.sum (λ (i : n), v i)
source
theorem matrix.one_dot_product {n : Type u_3} {α : Type v} [fintype n] [mul_one_class α] [add_comm_monoid α] (v : n → α) :
matrix.dot_product 1 v = finset.univ.sum (λ (i : n), v i)
source
@[simp]
theorem matrix.dot_product_zero {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (v : m → α) :
matrix.dot_product 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 → α) :
matrix.dot_product 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 → α) :
matrix.dot_product 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 → α) :
matrix.dot_product (λ (_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 → α) :
matrix.dot_product (u + v) w = matrix.dot_product u w + matrix.dot_product 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 → α) :
matrix.dot_product u (v + w) = matrix.dot_product u v + matrix.dot_product u w
source
@[simp]
theorem matrix.sum_elim_dot_product_sum_elim {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [non_unital_non_assoc_semiring α] (u v : m → α) (x y : n → α) :
matrix.dot_product (sum.elim u x) (sum.elim v y) = matrix.dot_product u v + matrix.dot_product x y
source
@[simp]
theorem matrix.comp_equiv_symm_dot_product {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [non_unital_non_assoc_semiring α] (u : m → α) (x : n → α) (e : m ≃ n) :
matrix.dot_product (u ∘ ⇑(e.symm)) x = matrix.dot_product u (x ∘ ⇑e)

Permuting a vector on the left of a dot product can be transferred to the right.

source
@[simp]
theorem matrix.dot_product_comp_equiv_symm {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [non_unital_non_assoc_semiring α] (u : m → α) (x : n → α) (e : n ≃ m) :
matrix.dot_product u (x ∘ ⇑(e.symm)) = matrix.dot_product (u ∘ ⇑e) x

Permuting a vector on the right of a dot product can be transferred to the left.

source
@[simp]
theorem matrix.comp_equiv_dot_product_comp_equiv {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [non_unital_non_assoc_semiring α] (x y : n → α) (e : m ≃ n) :
matrix.dot_product (x ∘ ⇑e) (y ∘ ⇑e) = matrix.dot_product x y

Permuting vectors on both sides of a dot product is a no-op.

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.dot_product (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) :
matrix.dot_product 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) :
matrix.dot_product 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) :
matrix.dot_product (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) :
matrix.dot_product v (pi.single i x) = v i * x
source
@[simp]
theorem matrix.one_dot_product_one {n : Type u_3} {α : Type v} [fintype n] [non_assoc_semiring α] :
matrix.dot_product 1 1 = ↑(fintype.card n)
source
@[simp]
theorem matrix.neg_dot_product {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_ring α] (v w : m → α) :
matrix.dot_product (-v) w = -matrix.dot_product v w
source
@[simp]
theorem matrix.dot_product_neg {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_ring α] (v w : m → α) :
matrix.dot_product v (-w) = -matrix.dot_product v w
source
@[simp]
theorem matrix.sub_dot_product {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_ring α] (u v w : m → α) :
matrix.dot_product (u - v) w = matrix.dot_product u w - matrix.dot_product v w
source
@[simp]
theorem matrix.dot_product_sub {m : Type u_2} {α : Type v} [fintype m] [non_unital_non_assoc_ring α] (u v w : m → α) :
matrix.dot_product u (v - w) = matrix.dot_product u v - matrix.dot_product 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 → α) :
matrix.dot_product (x • v) w = x • matrix.dot_product 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 → α) :
matrix.dot_product v (x • w) = x • matrix.dot_product v w
source
theorem matrix.star_dot_product_star {m : Type u_2} {α : Type v} [fintype m] [non_unital_semiring α] [star_ring α] (v w : m → α) :
matrix.dot_product (has_star.star v) (has_star.star w) = has_star.star (matrix.dot_product w v)
source
theorem matrix.star_dot_product {m : Type u_2} {α : Type v} [fintype m] [non_unital_semiring α] [star_ring α] (v w : m → α) :
matrix.dot_product (has_star.star v) w = has_star.star (matrix.dot_product (has_star.star w) v)
source
theorem matrix.dot_product_star {m : Type u_2} {α : Type v} [fintype m] [non_unital_semiring α] [star_ring α] (v w : m → α) :
matrix.dot_product v (has_star.star w) = has_star.star (matrix.dot_product w (has_star.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
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.mul N i k = finset.univ.sum (λ (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.mul 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.mul N i k = matrix.dot_product (λ (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 α) :
s.sum (λ (c : β), g c) i j = s.sum (λ (c : β), g c i j)
source
theorem matrix.two_mul_expl {R : Type u_1} [comm_ring R] (A B : matrix (fin 2) (fin 2) R) :
(A * B) 0 0 = A 0 0 * B 0 0 + A 0 1 * B 1 0 ∧ (A * B) 0 1 = A 0 0 * B 0 1 + A 0 1 * B 1 1 ∧ (A * B) 1 0 = A 1 0 * B 0 0 + A 1 1 * B 1 0 ∧ (A * B) 1 1 = A 1 0 * B 0 1 + A 1 1 * B 1 1
source
@[simp]
theorem matrix.smul_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [add_comm_monoid α] [has_mul α] [fintype n] [monoid R] [distrib_mul_action R α] [is_scalar_tower R α α] (a : R) (M : matrix m n α) (N : matrix n l α) :
(a • M).mul N = a • M.mul N
source
@[simp]
theorem matrix.mul_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [add_comm_monoid α] [has_mul α] [fintype n] [monoid R] [distrib_mul_action R α] [smul_comm_class R α α] (M : matrix m n α) (a : R) (N : matrix n l α) :
M.mul (a • N) = a • M.mul N
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.mul 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.mul 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.mul (M + N) = L.mul M + L.mul 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).mul N = L.mul N + M.mul 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).mul 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.mul (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₁).mul (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
theorem matrix.smul_eq_diagonal_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] [fintype m] [decidable_eq m] (M : matrix m n α) (a : α) :
a • M = (matrix.diagonal (λ (_x : m), a)).mul M
source
@[simp]
theorem matrix.diag_col_mul_row {n : Type u_3} {α : Type v} [non_unital_non_assoc_semiring α] (a b : n → α) :
((matrix.col a).mul (matrix.row b)).diag = a * b
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.mul 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.mul 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 α) :
(s.sum (λ (a : β), f a)).mul M = s.sum (λ (a : β), (f a).mul 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.mul (s.sum (λ (a : β), f a)) = s.sum (λ (a : β), M.mul (f a))
source
@[protected, instance]
def matrix.semiring.is_scalar_tower {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 α α] :
is_scalar_tower R (matrix n n α) (matrix n n α)

This instance enables use with smul_mul_assoc.

source
@[protected, instance]
def matrix.semiring.smul_comm_class {n : Type u_3} {R : Type u_7} {α : Type v} [non_unital_non_assoc_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
@[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.mul 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.mul 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.mul M).map ⇑f = (L.map ⇑f).mul (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.mul M).mul N = L.mul (M.mul 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
@[protected, simp]
theorem matrix.neg_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_ring α] [fintype n] (M : matrix m n α) (N : matrix n o α) :
(-M).mul N = -M.mul N
source
@[protected, simp]
theorem matrix.mul_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_ring α] [fintype n] (M : matrix m n α) (N : matrix n o α) :
M.mul (-N) = -M.mul N
source
@[protected]
theorem matrix.sub_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_ring α] [fintype n] (M M' : matrix m n α) (N : matrix n o α) :
(M - M').mul N = M.mul N - M'.mul N
source
@[protected]
theorem matrix.mul_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_non_assoc_ring α] [fintype n] (M : matrix m n α) (N N' : matrix n o α) :
M.mul (N - N') = M.mul N - M.mul N'
source
@[protected, instance]
def matrix.non_unital_non_assoc_ring {n : Type u_3} {α : Type v} [non_unital_non_assoc_ring α] [fintype n] :
non_unital_non_assoc_ring (matrix n n α)
Equations
source
@[protected, instance]
def matrix.non_unital_ring {n : Type u_3} {α : Type v} [fintype n] [non_unital_ring α] :
non_unital_ring (matrix n n α)
Equations
source
@[protected, instance]
def matrix.non_assoc_ring {n : Type u_3} {α : Type v} [fintype n] [decidable_eq n] [non_assoc_ring α] :
non_assoc_ring (matrix n n α)
Equations
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.diagonal_pow {n : Type u_3} {α : Type v} [semiring α] [fintype n] [decidable_eq n] (v : n → α) (k : ℕ) :
matrix.diagonal v ^ k = matrix.diagonal (v ^ k)
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 : α) :
(⇑matrix.of (λ (i : m) (j : n), a * M i j)).mul N = a • M.mul 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.mul (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.mul (⇑matrix.of (λ (i : n) (j : o), a * N i j)) = a • M.mul 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
theorem matrix.vec_mul_vec_apply {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] (w : m → α) (v : n → α) (i : m) (j : n) :
matrix.vec_mul_vec w v i j = w i * v j
source
theorem matrix.vec_mul_vec_eq {m : Type u_2} {n : Type u_3} {α : Type v} [has_mul α] [add_comm_monoid α] (w : m → α) (v : n → α) :
matrix.vec_mul_vec w v = (matrix.col w).mul (matrix.row v)
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) :
matrix.dot_product v (A.mul_vec w) = matrix.dot_product (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.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] [monoid R] [non_unital_non_assoc_semiring S] [distrib_mul_action R S] [is_scalar_tower R S 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] [monoid R] [non_unital_non_assoc_semiring S] [distrib_mul_action R S] [smul_comm_class R S 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.mul_vec_single {m : Type u_2} {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] [non_unital_non_assoc_semiring R] (M : matrix m n R) (j : n) (x : R) :
M.mul_vec (pi.single j x) = λ (i : m), M i j * x
source
@[simp]
theorem matrix.single_vec_mul {m : Type u_2} {n : Type u_3} {R : Type u_7} [fintype m] [decidable_eq m] [non_unital_non_assoc_semiring R] (M : matrix m n R) (i : m) (x : R) :
matrix.vec_mul (pi.single i x) M = λ (j : n), x * M i j
source
@[simp]
theorem matrix.diagonal_mul_vec_single {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] [non_unital_non_assoc_semiring R] (v : n → R) (j : n) (x : R) :
(matrix.diagonal v).mul_vec (pi.single j x) = pi.single j (v j * x)
source
@[simp]
theorem matrix.single_vec_mul_diagonal {n : Type u_3} {R : Type u_7} [fintype n] [decidable_eq n] [non_unital_non_assoc_semiring R] (v : n → R) (j : n) (x : R) :
matrix.vec_mul (pi.single j x) (matrix.diagonal v) = pi.single j (x * v j)
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.mul 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.mul N).mul_vec v
source
theorem matrix.star_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype n] [star_ring α] (M : matrix m n α) (v : n → α) :
has_star.star (M.mul_vec v) = matrix.vec_mul (has_star.star v) M.conj_transpose
source
theorem matrix.star_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype m] [star_ring α] (M : matrix m n α) (v : m → α) :
has_star.star (matrix.vec_mul v M) = M.conj_transpose.mul_vec (has_star.star v)
source
theorem matrix.mul_vec_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype m] [star_ring α] (A : matrix m n α) (x : m → α) :
A.conj_transpose.mul_vec x = has_star.star (matrix.vec_mul (has_star.star x) A)
source
theorem matrix.vec_mul_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype n] [star_ring α] (A : matrix m n α) (x : n → α) :
matrix.vec_mul x A.conj_transpose = has_star.star (A.mul_vec (has_star.star x))
source
theorem matrix.mul_mul_apply {n : Type u_3} {α : Type v} [non_unital_semiring α] [fintype n] (A B C : matrix n n α) (i j : n) :
(A.mul B).mul C i j = matrix.dot_product (A i) (B.mul_vec (C.transpose j))
source
theorem matrix.mul_vec_one {m : Type u_2} {n : Type u_3} {α : Type v} [non_assoc_semiring α] [fintype n] (A : matrix m n α) :
A.mul_vec 1 = λ (i : m), finset.univ.sum (λ (j : n), A i j)
source
theorem matrix.vec_one_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_assoc_semiring α] [fintype m] (A : matrix m n α) :
matrix.vec_mul 1 A = λ (j : n), finset.univ.sum (λ (i : m), A i j)
source
@[simp]
theorem matrix.one_mul_vec {m : Type u_2} {α : Type v} [non_assoc_semiring α] [fintype m] [decidable_eq m] (v : m → α) :
1.mul_vec v = v
source
@[simp]
theorem matrix.vec_mul_one {m : Type u_2} {α : Type v} [non_assoc_semiring α] [fintype m] [decidable_eq m] (v : m → α) :
matrix.vec_mul v 1 = v
source
theorem matrix.neg_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_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} [non_unital_non_assoc_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} [non_unital_non_assoc_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} [non_unital_non_assoc_ring α] [fintype n] (v : n → α) (A : matrix m n α) :
A.mul_vec (-v) = -A.mul_vec v
source
theorem matrix.sub_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_ring α] [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_sub {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_non_assoc_ring α] [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.mul_vec_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_comm_semiring α] [fintype m] (A : matrix m n α) (x : m → α) :
A.transpose.mul_vec x = matrix.vec_mul x A
source
theorem matrix.vec_mul_transpose {m : Type u_2} {n : Type u_3} {α : Type v} [non_unital_comm_semiring α] [fintype n] (A : matrix m n α) (x : n → α) :
matrix.vec_mul x A.transpose = A.mul_vec x
source
theorem matrix.mul_vec_vec_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_comm_semiring α] [fintype n] [fintype o] (A : matrix m n α) (B : matrix o n α) (x : o → α) :
A.mul_vec (matrix.vec_mul x B) = (A.mul B.transpose).mul_vec x
source
theorem matrix.vec_mul_mul_vec {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [non_unital_comm_semiring α] [fintype m] [fintype n] (A : matrix m n α) (B : matrix m o α) (x : n → α) :
matrix.vec_mul (A.mul_vec x) B = matrix.vec_mul x (A.transpose.mul B)
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
@[simp]
theorem matrix.transpose_transpose {m : Type u_2} {n : Type u_3} {α : Type v} (M : matrix m n α) :
M.transpose.transpose = M
source
@[simp]
theorem matrix.transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [has_zero α] :
0.transpose = 0
source
@[simp]
theorem matrix.transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] [has_one α] :
1.transpose = 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).transpose = M.transpose + N.transpose
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).transpose = M.transpose - N.transpose
source
@[simp]
theorem matrix.transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_monoid α] [comm_semigroup α] [fintype n] (M : matrix m n α) (N : matrix n l α) :
(M.mul N).transpose = N.transpose.mul M.transpose
source
@[simp]
theorem matrix.transpose_smul {m : Type u_2} {n : Type u_3} {α : Type v} {R : Type u_1} [has_smul R α] (c : R) (M : matrix m n α) :
(c • M).transpose = c • M.transpose
source
@[simp]
theorem matrix.transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [has_neg α] (M : matrix m n α) :
(-M).transpose = -M.transpose
source
theorem matrix.transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : matrix m n α} :
M.transpose.map f = (M.map f).transpose
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 n α) M = M.transpose
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 m n α).symm = matrix.transpose_add_equiv n m α
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.transpose = (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.transpose = (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 α) :
(s.sum (λ (i : ι), M i)).transpose = s.sum (λ (i : ι), (M i).transpose)
source
@[simp]
theorem matrix.transpose_linear_equiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [add_comm_monoid α] [module R α] (ᾰ : matrix m n α) :
⇑(matrix.transpose_linear_equiv m n R α) ᾰ = (matrix.transpose_add_equiv m n α).to_fun ᾰ
source
def matrix.transpose_linear_equiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [add_comm_monoid α] [module R α] :
matrix m n α ≃ₗ[R] matrix n m α

matrix.transpose as a linear_map

Equations
source
@[simp]
theorem matrix.transpose_linear_equiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [semiring R] [add_comm_monoid α] [module R α] :
(matrix.transpose_linear_equiv m n R α).symm = matrix.transpose_linear_equiv n m R α
source
def matrix.transpose_ring_equiv (m : Type u_2) (α : Type v) [add_comm_monoid α] [comm_semigroup α] [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) [add_comm_monoid α] [comm_semigroup α] [fintype m] (M : matrix m m α) :
⇑(matrix.transpose_ring_equiv m α) M = mul_opposite.op M.transpose
source
@[simp]
theorem matrix.transpose_ring_equiv_symm_apply (m : Type u_2) (α : Type v) [add_comm_monoid α] [comm_semigroup α] [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
⇑((matrix.transpose_ring_equiv m α).symm) M = (mul_opposite.unop M).transpose
source
@[simp]
theorem matrix.transpose_pow {m : Type u_2} {α : Type v} [comm_semiring α] [fintype m] [decidable_eq m] (M : matrix m m α) (k : ℕ) :
(M ^ k).transpose = M.transpose ^ k
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.transpose = (list.map matrix.transpose l).reverse.prod
source
@[simp]
theorem matrix.transpose_alg_equiv_symm_apply (m : Type u_2) (R : Type u_7) (α : Type v) [comm_semiring R] [comm_semiring α] [fintype m] [decidable_eq m] [algebra R α] (ᾰ : (matrix m m α)ᵐᵒᵖ) :
⇑((matrix.transpose_alg_equiv m R α).symm) ᾰ = ((matrix.transpose_add_equiv m m α).trans mul_opposite.op_add_equiv).inv_fun ᾰ
source
@[simp]
theorem matrix.transpose_alg_equiv_apply (m : Type u_2) (R : Type u_7) (α : Type v) [comm_semiring R] [comm_semiring α] [fintype m] [decidable_eq m] [algebra R α] (M : matrix m m α) :
⇑(matrix.transpose_alg_equiv m R α) M = mul_opposite.op M.transpose
source
def matrix.transpose_alg_equiv (m : Type u_2) (R : Type u_7) (α : Type v) [comm_semiring R] [comm_semiring α] [fintype m] [decidable_eq m] [algebra R α] :
matrix m m α ≃ₐ[R] (matrix m m α)ᵐᵒᵖ

matrix.transpose as an alg_equiv to the opposite ring

Equations
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.conj_transpose j 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.

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.conj_transpose.conj_transpose = M
source
@[simp]
theorem matrix.conj_transpose_zero {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] :
0.conj_transpose = 0
source
@[simp]
theorem matrix.conj_transpose_one {n : Type u_3} {α : Type v} [decidable_eq n] [semiring α] [star_ring α] :
1.conj_transpose = 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).conj_transpose = M.conj_transpose + N.conj_transpose
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).conj_transpose = M.conj_transpose - N.conj_transpose
source
@[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 α] [has_smul R α] [star_module R α] (c : R) (M : matrix m n α) :
(c • M).conj_transpose = has_star.star c • M.conj_transpose

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

source
@[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 α] [has_smul R α] [has_smul Rᵐᵒᵖ α] (c : R) (M : matrix m n α) (h : ∀ (r : R) (a : α), has_star.star (r • a) = mul_opposite.op (has_star.star r) • has_star.star a) :
(c • M).conj_transpose = mul_opposite.op (has_star.star c) • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_smul_self {m : Type u_2} {n : Type u_3} {α : Type v} [semigroup α] [star_semigroup α] (c : α) (M : matrix m n α) :
(c • M).conj_transpose = mul_opposite.op (has_star.star c) • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_nsmul {m : Type u_2} {n : Type u_3} {α : Type v} [add_monoid α] [star_add_monoid α] (c : ℕ) (M : matrix m n α) :
(c • M).conj_transpose = c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_zsmul {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] [star_add_monoid α] (c : ℤ) (M : matrix m n α) :
(c • M).conj_transpose = c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_nat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [semiring R] [add_comm_monoid α] [star_add_monoid α] [module R α] (c : ℕ) (M : matrix m n α) :
(↑c • M).conj_transpose = ↑c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_int_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [ring R] [add_comm_group α] [star_add_monoid α] [module R α] (c : ℤ) (M : matrix m n α) :
(↑c • M).conj_transpose = ↑c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_inv_nat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [division_semiring R] [add_comm_monoid α] [star_add_monoid α] [module R α] (c : ℕ) (M : matrix m n α) :
((↑c)⁻¹ • M).conj_transpose = (↑c)⁻¹ • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_inv_int_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [division_ring R] [add_comm_group α] [star_add_monoid α] [module R α] (c : ℤ) (M : matrix m n α) :
((↑c)⁻¹ • M).conj_transpose = (↑c)⁻¹ • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_rat_cast_smul {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [division_ring R] [add_comm_group α] [star_add_monoid α] [module R α] (c : ℚ) (M : matrix m n α) :
(↑c • M).conj_transpose = ↑c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_rat_smul {m : Type u_2} {n : Type u_3} {α : Type v} [add_comm_group α] [star_add_monoid α] [module ℚ α] (c : ℚ) (M : matrix m n α) :
(c • M).conj_transpose = c • M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [non_unital_semiring α] [star_ring α] (M : matrix m n α) (N : matrix n l α) :
(M.mul N).conj_transpose = N.conj_transpose.mul M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_neg {m : Type u_2} {n : Type u_3} {α : Type v} [add_group α] [star_add_monoid α] (M : matrix m n α) :
(-M).conj_transpose = -M.conj_transpose
source
theorem matrix.conj_transpose_map {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [has_star α] [has_star β] {A : matrix m n α} (f : α → β) (hf : function.semiconj f has_star.star has_star.star) :
A.conj_transpose.map f = (A.map f).conj_transpose
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 n α) M = M.conj_transpose
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 m n α).symm = matrix.conj_transpose_add_equiv n m α
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.conj_transpose = (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.conj_transpose = (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 α) :
(s.sum (λ (i : ι), M i)).conj_transpose = s.sum (λ (i : ι), (M i).conj_transpose)
source
@[simp]
theorem matrix.conj_transpose_linear_equiv_apply (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [comm_semiring R] [star_ring R] [add_comm_monoid α] [star_add_monoid α] [module R α] [star_module R α] (ᾰ : matrix m n α) :
⇑(matrix.conj_transpose_linear_equiv m n R α) ᾰ = (matrix.conj_transpose_add_equiv m n α).to_fun ᾰ
source
def matrix.conj_transpose_linear_equiv (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [comm_semiring R] [star_ring R] [add_comm_monoid α] [star_add_monoid α] [module R α] [star_module R α] :
matrix m n α ≃ₗ⋆[R] matrix n m α

matrix.conj_transpose as a linear_map

Equations
source
@[simp]
theorem matrix.conj_transpose_linear_equiv_symm (m : Type u_2) (n : Type u_3) (R : Type u_7) (α : Type v) [comm_semiring R] [star_ring R] [add_comm_monoid α] [star_add_monoid α] [module R α] [star_module R α] :
(matrix.conj_transpose_linear_equiv m n R α).symm = matrix.conj_transpose_linear_equiv n m R α
source
def matrix.conj_transpose_ring_equiv (m : Type u_2) (α : Type v) [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) [semiring α] [star_ring α] [fintype m] (M : matrix m m α) :
⇑(matrix.conj_transpose_ring_equiv m α) M = mul_opposite.op M.conj_transpose
source
@[simp]
theorem matrix.conj_transpose_ring_equiv_symm_apply (m : Type u_2) (α : Type v) [semiring α] [star_ring α] [fintype m] (M : (matrix m m α)ᵐᵒᵖ) :
⇑((matrix.conj_transpose_ring_equiv m α).symm) M = (mul_opposite.unop M).conj_transpose
source
@[simp]
theorem matrix.conj_transpose_pow {m : Type u_2} {α : Type v} [semiring α] [star_ring α] [fintype m] [decidable_eq m] (M : matrix m m α) (k : ℕ) :
(M ^ k).conj_transpose = M.conj_transpose ^ k
source
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 α)) :
l.prod.conj_transpose = (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 α) :
has_star.star M = M.conj_transpose
source
@[simp]
theorem matrix.star_apply {n : Type u_3} {α : Type v} [has_star α] (M : matrix n n α) (i j : n) :
has_star.star M i j = has_star.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_module {n : Type u_3} {α : Type v} {β : Type w} [has_star α] [has_star β] [has_smul α β] [star_module α β] :
star_module α (matrix n n β)
source
@[protected, instance]
def matrix.star_ring {n : Type u_3} {α : Type v} [fintype n] [non_unital_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] [non_unital_semiring α] [star_ring α] (M N : matrix n n α) :
has_star.star (M.mul N) = (has_star.star N).mul (has_star.star M)

A version of star_mul for ⬝ instead of *.

source
def matrix.submatrix {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.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
source
@[simp]
theorem matrix.submatrix_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.submatrix r_reindex c_reindex i j = A (r_reindex i) (c_reindex j)
source
@[simp]
theorem matrix.submatrix_id_id {m : Type u_2} {n : Type u_3} {α : Type v} (A : matrix m n α) :
A.submatrix id id = A
source
@[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 : matrix m 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₂)
source
@[simp]
theorem matrix.transpose_submatrix {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.submatrix r_reindex c_reindex).transpose = A.transpose.submatrix c_reindex r_reindex
source
@[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 : matrix m 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
source
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 : matrix m n α) :
(A + B).submatrix = A.submatrix + B.submatrix
source
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 : matrix m n α) :
(-A).submatrix = -A.submatrix
source
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 : matrix m n α) :
(A - B).submatrix = A.submatrix - B.submatrix
source
@[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 α] :
0.submatrix = 0
source
theorem matrix.submatrix_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {R : Type u_5} [has_smul R α] (r : R) (A : matrix m n α) :
(r • A).submatrix = r • A.submatrix
source
theorem matrix.submatrix_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).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f
source
theorem matrix.submatrix_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).submatrix 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.submatrix_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.submatrix e e = 1
source
theorem matrix.submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [has_mul α] [add_comm_monoid α] {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.mul N).submatrix e₁ e₃ = (M.submatrix e₁ e₂).mul (N.submatrix e₂ e₃)
source
theorem matrix.diag_submatrix {l : Type u_1} {m : Type u_2} {α : Type v} (A : matrix m m α) (e : l → m) :
(A.submatrix e e).diag = A.diag ∘ e

simp lemmas for matrix.submatrixs interaction with matrix.diagonal, 1, and matrix.mul for when the mappings are bundled.

source
@[simp]
theorem matrix.submatrix_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).submatrix ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
source
@[simp]
theorem matrix.submatrix_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).submatrix ⇑e ⇑e = matrix.diagonal (d ∘ ⇑e)
source
@[simp]
theorem matrix.submatrix_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.submatrix ⇑e ⇑e = 1
source
@[simp]
theorem matrix.submatrix_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.submatrix ⇑e ⇑e = 1
source
@[simp]
theorem matrix.submatrix_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [add_comm_monoid α] [has_mul α] {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.submatrix e₁ ⇑e₂).mul (N.submatrix ⇑e₂ e₃) = (M.mul N).submatrix e₁ e₃
source
theorem matrix.submatrix_mul_vec_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [fintype o] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : o → α) (e₁ : l → m) (e₂ : o ≃ n) :
(M.submatrix e₁ ⇑e₂).mul_vec v = M.mul_vec (v ∘ ⇑(e₂.symm)) ∘ e₁
source
theorem matrix.submatrix_vec_mul_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype l] [fintype m] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : l → α) (e₁ : l ≃ m) (e₂ : o → n) :
matrix.vec_mul v (M.submatrix ⇑e₁ e₂) = matrix.vec_mul (v ∘ ⇑(e₁.symm)) M ∘ e₂
source
theorem matrix.mul_submatrix_one {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype n] [finite o] [non_assoc_semiring α] [decidable_eq o] (e₁ : n ≃ o) (e₂ : l → o) (M : matrix m n α) :
M.mul (1.submatrix ⇑e₁ e₂) = M.submatrix id (⇑(e₁.symm) ∘ e₂)
source
theorem matrix.one_submatrix_mul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [fintype m] [finite o] [non_assoc_semiring α] [decidable_eq o] (e₁ : l → o) (e₂ : m ≃ o) (M : matrix m n α) :
(1.submatrix e₁ ⇑e₂).mul M = M.submatrix (⇑(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.submatrix ⇑(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).transpose = ⇑(matrix.reindex eₙ eₘ) M.transpose
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).conj_transpose = ⇑(matrix.reindex eₙ eₘ) M.conj_transpose
source
@[simp]
theorem matrix.submatrix_mul_transpose_submatrix {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [fintype n] [add_comm_monoid α] [has_mul α] (e : m ≃ n) (M : matrix m n α) :
(M.submatrix id ⇑e).mul (M.transpose.submatrix ⇑e id) = M.mul M.transpose
source
@[reducible]
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
@[reducible]
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
@[reducible]
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
@[reducible]
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
@[reducible]
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
@[reducible]
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
@[reducible]
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
@[reducible]
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_smul 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_smul R α] (x : R) (v : m → α) :
matrix.row (x • v) = x • matrix.row v
source
@[simp]
theorem matrix.transpose_col {m : Type u_2} {α : Type v} (v : m → α) :
(matrix.col v).transpose = matrix.row v
source
@[simp]
theorem matrix.transpose_row {m : Type u_2} {α : Type v} (v : m → α) :
(matrix.row v).transpose = matrix.col v
source
@[simp]
theorem matrix.conj_transpose_col {m : Type u_2} {α : Type v} [has_star α] (v : m → α) :
(matrix.col v).conj_transpose = matrix.row (has_star.star v)
source
@[simp]
theorem matrix.conj_transpose_row {m : Type u_2} {α : Type v} [has_star α] (v : m → α) :
(matrix.row v).conj_transpose = matrix.col (has_star.star v)
source
theorem matrix.row_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : m → α) :
matrix.row (matrix.vec_mul v M) = (matrix.row v).mul M
source
theorem matrix.col_vec_mul {m : Type u_2} {n : Type u_3} {α : Type v} [fintype m] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : m → α) :
matrix.col (matrix.vec_mul v M) = ((matrix.row v).mul M).transpose
source
theorem matrix.col_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : n → α) :
matrix.col (M.mul_vec v) = M.mul (matrix.col v)
source
theorem matrix.row_mul_vec {m : Type u_2} {n : Type u_3} {α : Type v} [fintype n] [non_unital_non_assoc_semiring α] (M : matrix m n α) (v : n → α) :
matrix.row (M.mul_vec v) = (M.mul (matrix.col v)).transpose
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).mul (matrix.col w) i j = matrix.dot_product v w
source
def matrix.update_row {m : Type u_2} {n : Type u_3} {α : Type v} [decidable_eq m] (M : matrix m n α) (i : m) (b : n → α) :
matrix m n α

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 n] (M : matrix m n α) (j : n) (b : m → α) :
matrix m n α

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 m n α} {i : m} {b : n → α} [decidable_eq m] :
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 m n α} {i : m} {j : n} {c : m → α} [decidable_eq n] :
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 m n α} {i : m} {b : n → α} [decidable_eq m] {i' : m} (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 m n α} {i : m} {j : n} {c : m → α} [decidable_eq n] {j' : n} (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 m n α} {i : m} {j : n} {b : n → α} [decidable_eq m] {i' : m} :
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 m n α} {i : m} {j : n} {c : m → α} [decidable_eq n] {j' : n} :
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 n] (A : matrix m n R) (i : n) (b : m → R) :
A.update_column i b = (matrix.col b).submatrix id (function.const n unit.star())
source
@[simp]
theorem matrix.update_row_subsingleton {m : Type u_2} {n : Type u_3} {R : Type u_7} [subsingleton m] (A : matrix m n R) (i : m) (b : n → R) :
A.update_row i b = (matrix.row b).submatrix (function.const m unit.star()) id
source
theorem matrix.map_update_row {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : matrix m n α} {i : m} {b : n → α} [decidable_eq m] (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 m n α} {j : n} {c : m → α} [decidable_eq n] (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 m n α} {j : n} {c : m → α} [decidable_eq n] :
M.transpose.update_row j c = (M.update_column j c).transpose
source
theorem matrix.update_column_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix m n α} {i : m} {b : n → α} [decidable_eq m] :
M.transpose.update_column i b = (M.update_row i b).transpose
source
theorem matrix.update_row_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix m n α} {j : n} {c : m → α} [decidable_eq n] [has_star α] :
M.conj_transpose.update_row j (has_star.star c) = (M.update_column j c).conj_transpose
source
theorem matrix.update_column_conj_transpose {m : Type u_2} {n : Type u_3} {α : Type v} {M : matrix m n α} {i : m} {b : n → α} [decidable_eq m] [has_star α] :
M.conj_transpose.update_column i (has_star.star b) = (M.update_row i b).conj_transpose
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 matrix.diagonal_update_column_single {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (v : n → α) (i : n) (x : α) :
(matrix.diagonal v).update_column i (pi.single i x) = matrix.diagonal (function.update v i x)
source
theorem matrix.diagonal_update_row_single {n : Type u_3} {α : Type v} [decidable_eq n] [has_zero α] (v : n → α) (i : n) (x : α) :
(matrix.diagonal v).update_row i (pi.single i x) = matrix.diagonal (function.update v i x)

Updating rows and columns commutes in the obvious way with reindexing the matrix.

source
theorem matrix.update_row_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq l] [decidable_eq m] (A : matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n) :
(A.submatrix ⇑e ⇑f).update_row i r = (A.update_row (⇑e i) (λ (j : n), r (⇑(f.symm) j))).submatrix ⇑e ⇑f
source
theorem matrix.submatrix_update_row_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq l] [decidable_eq m] (A : matrix m n α) (i : m) (r : n → α) (e : l ≃ m) (f : o ≃ n) :
(A.update_row i r).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).update_row (⇑(e.symm) i) (λ (i : o), r (⇑f i))
source
theorem matrix.update_column_submatrix_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq o] [decidable_eq n] (A : matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n) :
(A.submatrix ⇑e ⇑f).update_column j c = (A.update_column (⇑f j) (λ (i : m), c (⇑(e.symm) i))).submatrix ⇑e ⇑f
source
theorem matrix.submatrix_update_column_equiv {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq o] [decidable_eq n] (A : matrix m n α) (j : n) (c : m → α) (e : l ≃ m) (f : o ≃ n) :
(A.update_column j c).submatrix ⇑e ⇑f = (A.submatrix ⇑e ⇑f).update_column (⇑(f.symm) j) (λ (i : l), c (⇑e i))

reindex versions of the above submatrix lemmas for convenience.

source
theorem matrix.update_row_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq l] [decidable_eq m] (A : matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o) :
(⇑(matrix.reindex e f) A).update_row i r = ⇑(matrix.reindex e f) (A.update_row (⇑(e.symm) i) (λ (j : n), r (⇑f j)))
source
theorem matrix.reindex_update_row {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq l] [decidable_eq m] (A : matrix m n α) (i : m) (r : n → α) (e : m ≃ l) (f : n ≃ o) :
⇑(matrix.reindex e f) (A.update_row i r) = (⇑(matrix.reindex e f) A).update_row (⇑e i) (λ (i : o), r (⇑(f.symm) i))
source
theorem matrix.update_column_reindex {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq o] [decidable_eq n] (A : matrix m n α) (j : o) (c : l → α) (e : m ≃ l) (f : n ≃ o) :
(⇑(matrix.reindex e f) A).update_column j c = ⇑(matrix.reindex e f) (A.update_column (⇑(f.symm) j) (λ (i : m), c (⇑e i)))
source
theorem matrix.reindex_update_column {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [decidable_eq o] [decidable_eq n] (A : matrix m n α) (j : n) (c : m → α) (e : m ≃ l) (f : n ≃ o) :
⇑(matrix.reindex e f) (A.update_column j c) = (⇑(matrix.reindex e f) A).update_column (⇑f j) (λ (i : l), c (⇑(e.symm) i))
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] [non_assoc_semiring α] [non_assoc_semiring β] (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f : α →+* β) :
⇑f (M.mul N i j) = (M.map ⇑f).mul (N.map ⇑f) i j
source
theorem ring_hom.map_dot_product {n : Type u_3} {R : Type u_7} {S : Type u_8} [fintype n] [non_assoc_semiring R] [non_assoc_semiring S] (f : R →+* S) (v w : n → R) :
⇑f (matrix.dot_product v w) = matrix.dot_product (⇑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] [non_assoc_semiring R] [non_assoc_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] [non_assoc_semiring R] [non_assoc_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