Documentation

Seymour.Matrix.Basic

Basic stuff about matrices #

This file provides a specific API about matrices for the purposes of our project.

source
@[simp]
theorem Matrix.one_fromCols_transpose {α : Type u_1} [Zero α] [One α] {m : Type u_2} {n : Type u_3} [DecidableEq m] (A : Matrix m n α) :
(1 ◫ A).transpose = 1 ⊟ A.transpose
source
@[simp]
theorem Matrix.one_fromRows_transpose {α : Type u_1} [Zero α] [One α] {m : Type u_2} {n : Type u_3} [DecidableEq n] (A : Matrix m n α) :
(1 ⊟ A).transpose = 1 ◫ A.transpose
source
@[simp]
theorem Matrix.fromCols_one_transpose {α : Type u_1} [Zero α] [One α] {m : Type u_2} {n : Type u_3} [DecidableEq m] (A : Matrix m n α) :
(A ◫ 1).transpose = A.transpose ⊟ 1
source
@[simp]
theorem Matrix.fromRows_one_transpose {α : Type u_1} [Zero α] [One α] {m : Type u_2} {n : Type u_3} [DecidableEq n] (A : Matrix m n α) :
(A ⊟ 1).transpose = A.transpose ◫ 1
source
theorem Matrix.ext_col {α : Type u_1} {m : Type u_2} {n : Type u_3} {A B : Matrix m n α} (hAB : ∀ (i : m), A i = B i) :
A = B

Two matrices are equal if they agree on all columns.

source
theorem Matrix.det_int_coe {α : Type u_1} [DecidableEq α] [Fintype α] (A : Matrix α α ℤ) (F : Type u_2) [Field F] :
↑A.det = (A.map Int.cast).det

Computing the determinant of a square integer matrix and then converting it to a general field gives the same result as converting all elements to given field and computing the determinant afterwards.

source
theorem Matrix.entrywiseProduct_outerProduct_eq_mul_col_mul_row {α : Type u_1} {m : Type u_2} {n : Type u_3} [Semigroup α] (A : Matrix m n α) (c : m → α) (r : n → α) :
A ⊡ c ⊗ r = of fun (i : m) (j : n) => A i j * c i * r j
source
theorem Matrix.entrywiseProduct_outerProduct_eq_mul_row_mul_col {α : Type u_1} {m : Type u_2} {n : Type u_3} [CommSemigroup α] (A : Matrix m n α) (c : m → α) (r : n → α) :
A ⊡ c ⊗ r = of fun (i : m) (j : n) => A i j * r j * c i
source
theorem sum_elem_smul_matrix_row_of_mem {α : Type u_1} [DecidableEq α] {β : Type u_2} [NonAssocSemiring β] {x : α} {S : Set α} [Fintype ↑S] (f : α → β) (hxS : x ∈ S) :
∑ i : ↑S, f ↑i • 1 x ↑i = f x
source
theorem sum_elem_smul_matrix_row_of_nmem {α : Type u_1} [DecidableEq α] {β : Type u_2} [NonAssocSemiring β] {x : α} {S : Set α} [Fintype ↑S] (f : α → β) (hxS : x ∉ S) :
∑ i : ↑S, f ↑i • 1 x ↑i = 0
source
def Matrix.abs {α : Type u_1} [LinearOrderedAddCommGroup α] {m : Type u_2} {n : Type u_3} (A : Matrix m n α) :
Matrix m n α

The absolute value of a matrix is a matrix made of absolute values of respective elements.

Equations
Instances For
    source
    def «term|___|_1» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For