Mathlib.Data.Matrix.RowCol

Matrix.replicateCol definition

(ι : Type*) (w : m → α) : Matrix m ι α

Full source

/--
`Matrix.replicateCol ι u` is the matrix with all columns equal to the vector `u`.

To get a column matrix with exactly one column,
`Matrix.replicateCol (Fin 1) u` is the canonical choice.
-/
def replicateCol (ι : Type*) (w : m → α) : Matrix m ι α :=
  of fun x _ => w x

Matrix with replicated columns

Informal description

Given a type $\iota$ and a vector $w : m \to \alpha$, the function `Matrix.replicateCol ι w` constructs a matrix of type $m \times \iota \to \alpha$ where every column is equal to the vector $w$. Specifically, for any $i \in m$ and $j \in \iota$, the entry at position $(i, j)$ in the matrix is given by $w(i)$.

Matrix.replicateCol_apply theorem

{ι : Type*} (w : m → α) (i) (j : ι) : replicateCol ι w i j = w i

Full source

@[simp]
theorem replicateCol_apply {ι : Type*} (w : m → α) (i) (j : ι) : replicateCol ι w i j = w i :=
  rfl

Entry Formula for Matrix with Replicated Columns

Informal description

For any vector $w : m \to \alpha$, index $i \in m$, and index $j \in \iota$, the entry at position $(i, j)$ in the matrix $\text{replicateCol}_\iota w$ is equal to $w(i)$. That is, $(\text{replicateCol}_\iota w)_{i,j} = w(i)$.

Matrix.replicateRow definition

(ι : Type*) (v : n → α) : Matrix ι n α

Full source

/--
`Matrix.replicateRow ι u` is the matrix with all rows equal to the vector `u`.

To get a row matrix with exactly one row, `Matrix.replicateRow (Fin 1) u` is the canonical choice.
-/
def replicateRow (ι : Type*) (v : n → α) : Matrix ι n α :=
  of fun _ y => v y

Matrix with replicated rows

Informal description

Given a type $\iota$ and a vector $v : n \to \alpha$, the function `Matrix.replicateRow ι v` constructs a matrix of type $\iota \times n \to \alpha$ where every row is equal to the vector $v$. Specifically, for any $i \in \iota$ and $j \in n$, the entry at position $(i, j)$ in the matrix is given by $v(j)$.

Matrix.replicateRow_apply theorem

(v : n → α) (i : ι) (j) : replicateRow ι v i j = v j

Full source

@[simp]
theorem replicateRow_apply (v : n → α) (i : ι) (j) : replicateRow ι v i j = v j :=
  rfl

Entry Formula for Matrix with Replicated Rows

Informal description

For any vector $v : n \to \alpha$, index $i \in \iota$, and index $j \in n$, the entry at position $(i, j)$ in the matrix `replicateRow ι v` is equal to $v(j)$. That is, $\text{replicateRow}_\iota v\, i\, j = v(j)$.

Matrix.replicateCol_injective theorem

[Nonempty ι] : Function.Injective (replicateCol ι : (m → α) → Matrix m ι α)

Full source

theorem replicateCol_injective [Nonempty ι] :
    Function.Injective (replicateCol ι : (m → α) → Matrix m ι α) := by
  inhabit ι
  exact fun _x _y h => funext fun i => congr_fun₂ h i default

Injectivity of Column Replication in Nonempty Matrices

Informal description

For any nonempty type $\iota$, the function that constructs a matrix by replicating a vector $w : m \to \alpha$ as columns is injective. That is, if two vectors $v, w : m \to \alpha$ satisfy $\text{replicateCol}_\iota v = \text{replicateCol}_\iota w$, then $v = w$.

Matrix.replicateCol_inj theorem

[Nonempty ι] {v w : m → α} : replicateCol ι v = replicateCol ι w ↔ v = w

Full source

@[simp] theorem replicateCol_inj [Nonempty ι] {v w : m → α} :
    replicateColreplicateCol ι v = replicateCol ι w ↔ v = w :=
  replicateCol_injective.eq_iff

Equality of Replicated Column Matrices iff Equality of Vectors

Informal description

For any nonempty type $\iota$ and any two vectors $v, w : m \to \alpha$, the matrices formed by replicating $v$ and $w$ as columns are equal if and only if the vectors themselves are equal, i.e., $\text{replicateCol}_\iota v = \text{replicateCol}_\iota w \leftrightarrow v = w$.

Matrix.replicateCol_zero theorem

[Zero α] : replicateCol ι (0 : m → α) = 0

Full source

@[simp] theorem replicateCol_zero [Zero α] : replicateCol ι (0 : m → α) = 0 := rfl

Replicated Zero Columns Yield Zero Matrix

Informal description

For any type $\iota$ and any zero element $0$ in a type $\alpha$ with a zero structure, the matrix formed by replicating the zero vector $0 : m \to \alpha$ as columns is equal to the zero matrix of type $m \times \iota \to \alpha$.

Matrix.replicateCol_eq_zero theorem

[Zero α] [Nonempty ι] (v : m → α) : replicateCol ι v = 0 ↔ v = 0

Full source

@[simp] theorem replicateCol_eq_zero [Zero α] [Nonempty ι] (v : m → α) :
    replicateColreplicateCol ι v = 0 ↔ v = 0 :=
  replicateCol_inj

Zero Matrix Condition for Replicated Columns: $\text{replicateCol}_\iota v = 0 \leftrightarrow v = 0$

Informal description

For any type $\alpha$ with a zero element and any nonempty type $\iota$, a matrix formed by replicating a vector $v : m \to \alpha$ as columns is equal to the zero matrix if and only if the vector $v$ is identically zero. That is, $\text{replicateCol}_\iota v = 0 \leftrightarrow v = 0$.

Matrix.replicateCol_add theorem

[Add α] (v w : m → α) : replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

Full source

@[simp]
theorem replicateCol_add [Add α] (v w : m → α) :
    replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w := by
  ext
  rfl

Additivity of Column Replication: $\text{replicateCol}_\iota (v + w) = \text{replicateCol}_\iota v + \text{replicateCol}_\iota w$

Informal description

For any type $\iota$ and any vectors $v, w : m \to \alpha$ in an additive structure, the matrix formed by replicating the sum of vectors $v + w$ as columns is equal to the sum of the matrices formed by replicating $v$ and $w$ separately as columns. That is, $\text{replicateCol}_\iota (v + w) = \text{replicateCol}_\iota v + \text{replicateCol}_\iota w$.

Matrix.replicateCol_smul theorem

[SMul R α] (x : R) (v : m → α) : replicateCol ι (x • v) = x • replicateCol ι v

Full source

@[simp]
theorem replicateCol_smul [SMul R α] (x : R) (v : m → α) :
    replicateCol ι (x • v) = x • replicateCol ι v := by
  ext
  rfl

Scalar Multiplication Commutes with Column Replication: $\text{replicateCol}_\iota (x \cdot v) = x \cdot \text{replicateCol}_\iota v$

Informal description

For any scalar $x$ in a type $R$ with a scalar multiplication operation on $\alpha$, and any vector $v : m \to \alpha$, the matrix obtained by replicating the scaled vector $x \cdot v$ as columns is equal to the scalar multiple $x$ of the matrix obtained by replicating $v$ as columns. That is, $\text{replicateCol}_\iota (x \cdot v) = x \cdot \text{replicateCol}_\iota v$.

Matrix.replicateRow_injective theorem

[Nonempty ι] : Function.Injective (replicateRow ι : (n → α) → Matrix ι n α)

Full source

theorem replicateRow_injective [Nonempty ι] :
    Function.Injective (replicateRow ι : (n → α) → Matrix ι n α) := by
  inhabit ι
  exact fun _x _y h => funext fun j => congr_fun₂ h default j

Injectivity of Row Replication in Matrices

Informal description

For any nonempty type $\iota$, the function that constructs a matrix with all rows equal to a given vector $v : n \to \alpha$ is injective. That is, if two matrices constructed by replicating rows from vectors $v$ and $w$ are equal, then $v = w$.

Matrix.replicateRow_inj theorem

[Nonempty ι] {v w : n → α} : replicateRow ι v = replicateRow ι w ↔ v = w

Full source

@[simp] theorem replicateRow_inj [Nonempty ι] {v w : n → α} :
    replicateRowreplicateRow ι v = replicateRow ι w ↔ v = w :=
  replicateRow_injective.eq_iff

Equality of Replicated Row Matrices iff Vector Equality

Informal description

For any nonempty type $\iota$ and any two vectors $v, w : n \to \alpha$, the matrix with all rows equal to $v$ is identical to the matrix with all rows equal to $w$ if and only if $v = w$. In other words, $\text{replicateRow}_\iota v = \text{replicateRow}_\iota w \leftrightarrow v = w$.

Matrix.replicateRow_zero theorem

[Zero α] : replicateRow ι (0 : n → α) = 0

Full source

@[simp] theorem replicateRow_zero [Zero α] : replicateRow ι (0 : n → α) = 0 := rfl

Zero Vector Replication Yields Zero Matrix

Informal description

For any type $\iota$ and any type $n$, if $\alpha$ has a zero element, then the matrix with all rows equal to the zero vector $0 : n \to \alpha$ is equal to the zero matrix.

Matrix.replicateRow_eq_zero theorem

[Zero α] [Nonempty ι] (v : n → α) : replicateRow ι v = 0 ↔ v = 0

Full source

@[simp] theorem replicateRow_eq_zero [Zero α] [Nonempty ι] (v : n → α) :
    replicateRowreplicateRow ι v = 0 ↔ v = 0 :=
  replicateRow_inj

Zero Matrix Condition for Replicated Row Matrices: $\text{replicateRow}_\iota v = 0 \leftrightarrow v = 0$

Informal description

For any type $\alpha$ with a zero element and any nonempty type $\iota$, a matrix with all rows equal to a vector $v : n \to \alpha$ is the zero matrix if and only if $v$ is the zero vector. That is, $\text{replicateRow}_\iota v = 0 \leftrightarrow v = 0$.

Matrix.replicateRow_add theorem

[Add α] (v w : m → α) : replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

Full source

@[simp]
theorem replicateRow_add [Add α] (v w : m → α) :
    replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w := by
  ext
  rfl

Additivity of Row-Replicated Matrices: $\text{replicateRow}_\iota (v + w) = \text{replicateRow}_\iota v + \text{replicateRow}_\iota w$

Informal description

For any type $\iota$ and any additive structure on $\alpha$, given two vectors $v, w : m \to \alpha$, the matrix with all rows equal to the sum $v + w$ is equal to the sum of the matrices with all rows equal to $v$ and $w$ respectively. That is, \[ \text{replicateRow}_\iota (v + w) = \text{replicateRow}_\iota v + \text{replicateRow}_\iota w. \]

Matrix.replicateRow_smul theorem

[SMul R α] (x : R) (v : m → α) : replicateRow ι (x • v) = x • replicateRow ι v

Full source

@[simp]
theorem replicateRow_smul [SMul R α] (x : R) (v : m → α) :
    replicateRow ι (x • v) = x • replicateRow ι v := by
  ext
  rfl

Scalar Multiplication Commutes with Row Replication in Matrices

Informal description

Let $R$ and $\alpha$ be types equipped with a scalar multiplication operation, and let $\iota$ and $m$ be arbitrary types. For any scalar $x \in R$ and any vector $v : m \to \alpha$, the row-replicated matrix formed from the scalar multiple $x \cdot v$ is equal to the scalar multiple $x$ applied to the row-replicated matrix formed from $v$. That is, $\text{replicateRow}_\iota (x \cdot v) = x \cdot \text{replicateRow}_\iota v$.

Matrix.transpose_replicateCol theorem

(v : m → α) : (replicateCol ι v)ᵀ = replicateRow ι v

Full source

@[simp]
theorem transpose_replicateCol (v : m → α) : (replicateCol ι v)ᵀ = replicateRow ι v := by
  ext
  rfl

Transpose of Column-Replicated Matrix Equals Row-Replicated Matrix

Informal description

For any vector $v : m \to \alpha$, the transpose of the matrix `replicateCol ι v` (where every column is $v$) is equal to the matrix `replicateRow ι v` (where every row is $v$).

Matrix.transpose_replicateRow theorem

(v : m → α) : (replicateRow ι v)ᵀ = replicateCol ι v

Full source

@[simp]
theorem transpose_replicateRow (v : m → α) : (replicateRow ι v)ᵀ = replicateCol ι v := by
  ext
  rfl

Transpose of Row-Replicated Matrix Equals Column-Replicated Matrix

Informal description

For any vector $v : m \to \alpha$, the transpose of the row-replicated matrix $\text{replicateRow}_\iota v$ (where every row is $v$) is equal to the column-replicated matrix $\text{replicateCol}_\iota v$ (where every column is $v$).

Matrix.conjTranspose_replicateCol theorem

[Star α] (v : m → α) : (replicateCol ι v)ᴴ = replicateRow ι (star v)

Full source

@[simp]
theorem conjTranspose_replicateCol [Star α] (v : m → α) :
    (replicateCol ι v)ᴴ = replicateRow ι (star v) := by
  ext
  rfl

Conjugate Transpose of Column-Replicated Matrix Equals Row-Replicated Starred Vector

Informal description

For any type $\iota$, any vector $v : m \to \alpha$ in a star-semigroup $\alpha$, the conjugate transpose of the column-replicated matrix $\text{replicateCol}_\iota v$ is equal to the row-replicated matrix $\text{replicateRow}_\iota (\star \circ v)$, where $\star$ denotes the star operation on $\alpha$.

Matrix.conjTranspose_replicateRow theorem

[Star α] (v : m → α) : (replicateRow ι v)ᴴ = replicateCol ι (star v)

Full source

@[simp]
theorem conjTranspose_replicateRow [Star α] (v : m → α) :
    (replicateRow ι v)ᴴ = replicateCol ι (star v) := by
  ext
  rfl

Conjugate Transpose of Row-Replicated Matrix Equals Column-Replicated Starred Vector

Informal description

For any type $\iota$, any vector $v : m \to \alpha$ in a star-semigroup $\alpha$, the conjugate transpose of the row-replicated matrix $\text{replicateRow}_\iota v$ is equal to the column-replicated matrix $\text{replicateCol}_\iota (\star \circ v)$, where $\star$ denotes the star operation on $\alpha$.

Matrix.replicateRow_vecMul theorem

 [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
  replicateRow ι (v ᵥ* M) = replicateRow ι v * M

Full source

theorem replicateRow_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α)
    (v : m → α) : replicateRow ι (v ᵥ* M) = replicateRow ι v * M := by
  ext
  rfl

Row-Replicated Vector-Matrix Product Equals Matrix Product of Row-Replicated Vector

Informal description

Let $m$ and $n$ be finite types, $\alpha$ a non-unital non-associative semiring, $M$ an $m \times n$ matrix over $\alpha$, and $v : m \to \alpha$ a vector. Then the row-replicated matrix of the vector-matrix product $v \cdot M$ is equal to the matrix product of the row-replicated matrix of $v$ with $M$, i.e., \[ \text{replicateRow}_\iota (v \cdot M) = \text{replicateRow}_\iota v \cdot M. \]

Matrix.replicateCol_vecMul theorem

 [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : m → α) :
  replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ

Full source

theorem replicateCol_vecMul [Fintype m] [NonUnitalNonAssocSemiring α] (M : Matrix m n α)
    (v : m → α) : replicateCol ι (v ᵥ* M) = (replicateRow ι v * M)ᵀ := by
  ext
  rfl

Vector-Matrix Product Replicated as Column Matrix Equals Transposed Row-Matrix Product

Informal description

Let $m$ and $n$ be finite types, $\alpha$ a non-unital non-associative semiring, $M$ an $m \times n$ matrix over $\alpha$, and $v : m \to \alpha$ a vector. Then the vector-matrix product $v \cdot M$ replicated as a column matrix equals the transpose of the matrix product of the row matrix formed by replicating $v$ across all rows multiplied by $M$, i.e., \[ \text{replicateCol}_\iota (v \cdot M) = (\text{replicateRow}_\iota v \cdot M)^T. \]

Matrix.replicateCol_mulVec theorem

 [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
  replicateCol ι (M *ᵥ v) = M * replicateCol ι v

Full source

theorem replicateCol_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α)
    (v : n → α) : replicateCol ι (M *ᵥ v) = M * replicateCol ι v := by
  ext
  rfl

Matrix-Vector Product Equals Matrix Multiplication with Replicated Columns

Informal description

Let $M$ be an $m \times n$ matrix over a non-unital non-associative semiring $\alpha$, and let $v$ be a vector in $\alpha^n$. Then the matrix-vector product $M \cdot v$ is equal to the matrix product $M$ multiplied by the column matrix formed by replicating $v$ across all columns, i.e., \[ \text{replicateCol}_\iota (M \cdot v) = M \cdot \text{replicateCol}_\iota v. \]

Matrix.replicateRow_mulVec theorem

 [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α) (v : n → α) :
  replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ

Full source

theorem replicateRow_mulVec [Fintype n] [NonUnitalNonAssocSemiring α] (M : Matrix m n α)
    (v : n → α) : replicateRow ι (M *ᵥ v) = (M * replicateCol ι v)ᵀ := by
  ext
  rfl

Row Replication of Matrix-Vector Product Equals Transposed Matrix Multiplication with Replicated Columns

Informal description

Let $m$ and $n$ be finite types, $\alpha$ a non-unital non-associative semiring, $M$ an $m \times n$ matrix over $\alpha$, and $v : n \to \alpha$ a vector. Then the matrix-vector product $M \cdot v$ replicated as a row matrix equals the transpose of the matrix product $M$ multiplied by the column matrix formed by replicating $v$ across all columns, i.e., \[ \text{replicateRow}_\iota (M \cdot v) = (M \cdot \text{replicateCol}_\iota v)^T. \]

Matrix.replicateRow_mulVec_eq_const theorem

[Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) : replicateRow ι v *ᵥ w = Function.const _ (v ⬝ᵥ w)

Full source

theorem replicateRow_mulVec_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
    replicateRowreplicateRow ι v *ᵥ w = Function.const _ (v ⬝ᵥ w) := rfl

Matrix-Vector Product of Replicated Rows Equals Constant Dot Product

Informal description

Let $m$ be a finite type and $\alpha$ a non-unital non-associative semiring. For any vectors $v, w : m \to \alpha$, the matrix-vector product of the row-replicated matrix $\text{replicateRow}_\iota v$ with $w$ equals the constant function that maps every index to the dot product $v \cdot w$, i.e., \[ \text{replicateRow}_\iota v \cdot w = \text{const}_\iota (v \cdot w). \]

Matrix.mulVec_replicateCol_eq_const theorem

[Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) : v ᵥ* replicateCol ι w = Function.const _ (v ⬝ᵥ w)

Full source

theorem mulVec_replicateCol_eq_const [Fintype m] [NonUnitalNonAssocSemiring α] (v w : m → α) :
    v ᵥ* replicateCol ι w = Function.const _ (v ⬝ᵥ w) := rfl

Matrix-vector product with replicated columns equals constant dot product

Informal description

Let $m$ be a finite type, $\alpha$ a non-unital non-associative semiring, and $v, w : m \to \alpha$ be vectors. Then the matrix-vector product of $v$ with the matrix `replicateCol ι w` (where every column is $w$) equals the constant function that maps every index to the dot product $v \cdot w$.

Matrix.replicateRow_mul_replicateCol theorem

 [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) : replicateRow ι v * replicateCol ι w = of fun _ _ => v ⬝ᵥ w

Full source

theorem replicateRow_mul_replicateCol [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) :
    replicateRow ι v * replicateCol ι w = of fun _ _ => v ⬝ᵥ w :=
  rfl

Product of Replicated Row and Column Matrices Equals Constant Dot Product Matrix

Informal description

Let $m$ be a finite type, $\alpha$ a type equipped with multiplication and an additive commutative monoid structure, and $v, w : m \to \alpha$ be vectors. The matrix product of the row-replicated matrix $\text{replicateRow}_\iota v$ and the column-replicated matrix $\text{replicateCol}_\iota w$ is equal to the matrix where every entry is the dot product $v \cdot w$.

Matrix.replicateRow_mul_replicateCol_apply theorem

 [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α) (i j) : (replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w

Full source

@[simp]
theorem replicateRow_mul_replicateCol_apply [Fintype m] [Mul α] [AddCommMonoid α] (v w : m → α)
    (i j) : (replicateRow ι v * replicateCol ι w) i j = v ⬝ᵥ w :=
  rfl

Matrix Entry of Product of Replicated Row and Column Matrices Equals Dot Product

Informal description

Let $m$ be a finite type, $\alpha$ a type equipped with multiplication and an additive commutative monoid structure, and $v, w : m \to \alpha$ be vectors. For any indices $i$ and $j$, the $(i,j)$-th entry of the matrix product $\text{replicateRow}_\iota v \cdot \text{replicateCol}_\iota w$ is equal to the dot product $v \cdot w$.

Matrix.diag_replicateCol_mul_replicateRow theorem

[Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) : diag (replicateCol ι a * replicateRow ι b) = a * b

Full source

@[simp]
theorem diag_replicateCol_mul_replicateRow [Mul α] [AddCommMonoid α] [Unique ι] (a b : n → α) :
    diag (replicateCol ι a * replicateRow ι b) = a * b := by
  ext
  simp [Matrix.mul_apply, replicateCol, replicateRow]

Diagonal of Product of Replicated Column and Row Matrices Equals Pointwise Product

Informal description

Let $\alpha$ be a type with multiplication and an additive commutative monoid structure, and let $\iota$ be a type with a unique element. For any vectors $a, b : n \to \alpha$, the diagonal of the matrix product $\text{replicateCol}_\iota a \cdot \text{replicateRow}_\iota b$ is equal to the pointwise product $a \cdot b$.

Matrix.vecMulVec_eq theorem

 [Mul α] [AddCommMonoid α] [Unique ι] (w : m → α) (v : n → α) : vecMulVec w v = replicateCol ι w * replicateRow ι v

Full source

theorem vecMulVec_eq [Mul α] [AddCommMonoid α] [Unique ι] (w : m → α) (v : n → α) :
    vecMulVec w v = replicateCol ι w * replicateRow ι v := by
  ext
  simp [vecMulVec, mul_apply]

Outer Product as Matrix Multiplication of Replicated Column and Row Matrices

Informal description

Let $\alpha$ be a type with multiplication and an additive commutative monoid structure, and let $\iota$ be a type with a unique element. For any vectors $w : m \to \alpha$ and $v : n \to \alpha$, the outer product $\text{vecMulVec}(w, v)$ is equal to the matrix product $\text{replicateCol}_\iota w \cdot \text{replicateRow}_\iota v$.

Matrix.updateRow definition

[DecidableEq m] (M : Matrix m n α) (i : m) (b : n → α) : Matrix m n α

Full source

/-- Update, i.e. replace the `i`th row of matrix `A` with the values in `b`. -/
def updateRow [DecidableEq m] (M : Matrix m n α) (i : m) (b : n → α) : Matrix m n α :=
  of <| Function.update M i b

Matrix row update

Informal description

Given a matrix $ M $ of size $ m \times n $ with entries in $ \alpha $, a row index $ i $, and a vector $ b $ of length $ n $, the function `Matrix.updateRow` returns a new matrix where the $ i $-th row of $ M $ is replaced by $ b $. The resulting matrix has the same dimensions as $ M $.

Matrix.updateCol definition

[DecidableEq n] (M : Matrix m n α) (j : n) (b : m → α) : Matrix m n α

Full source

/-- Update, i.e. replace the `j`th column of matrix `A` with the values in `b`. -/
def updateCol [DecidableEq n] (M : Matrix m n α) (j : n) (b : m → α) : Matrix m n α :=
  of fun i => Function.update (M i) j (b i)

Matrix column update

Informal description

Given a matrix $ M $ of size $ m \times n $ with entries in $ \alpha $, a column index $ j $, and a vector $ b $ of length $ m $, the function `Matrix.updateCol` returns a new matrix where the $ j $-th column of $ M $ is replaced by $ b $. The resulting matrix has the same dimensions as $ M $.

Matrix.updateRow_self theorem

[DecidableEq m] : updateRow M i b i = b

Full source

@[simp]
theorem updateRow_self [DecidableEq m] : updateRow M i b i = b :=
  Function.update_self (β := fun _ => (n → α)) i b M

Updated Row Matches Input Vector

Informal description

For any matrix $M$ of size $m \times n$ with entries in $\alpha$, any row index $i$, and any vector $b$ of length $n$, updating the $i$-th row of $M$ to $b$ results in a new matrix whose $i$-th row is exactly $b$.

Matrix.updateCol_self theorem

[DecidableEq n] : updateCol M j c i j = c i

Full source

@[simp]
theorem updateCol_self [DecidableEq n] : updateCol M j c i j = c i :=
  Function.update_self (β := fun _ => α) j (c i) (M i)

Updated Column Entry Matches Input Vector Component

Informal description

For any matrix $M$ of size $m \times n$ with entries in a type $\alpha$, any column index $j$, and any vector $c : m \to \alpha$, updating the $j$-th column of $M$ with $c$ results in a new matrix where the entry at row $i$ and column $j$ is equal to $c_i$.

Matrix.updateRow_ne theorem

[DecidableEq m] {i' : m} (i_ne : i' ≠ i) : updateRow M i b i' = M i'

Full source

@[simp]
theorem updateRow_ne [DecidableEq m] {i' : m} (i_ne : i' ≠ i) : updateRow M i b i' = M i' :=
  Function.update_of_ne (β := fun _ => (n → α)) i_ne b M

Matrix Row Update Preserves Other Rows

Informal description

For any matrix $M$ of size $m \times n$ with entries in a type $\alpha$, any row index $i$, any vector $b$ of length $n$, and any distinct row index $i' \neq i$, updating the $i$-th row of $M$ to $b$ preserves the $i'$-th row, i.e., $\text{updateRow } M \, i \, b \, i' = M \, i'$.

Matrix.updateCol_ne theorem

[DecidableEq n] {j' : n} (j_ne : j' ≠ j) : updateCol M j c i j' = M i j'

Full source

@[simp]
theorem updateCol_ne [DecidableEq n] {j' : n} (j_ne : j' ≠ j) :
    updateCol M j c i j' = M i j' :=
  Function.update_of_ne (β := fun _ => α) j_ne (c i) (M i)

Matrix Column Update Preserves Entries in Other Columns

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, and let $j'$ be a column index distinct from $j$ (i.e., $j' \neq j$). Then updating the $j$-th column of $M$ with a vector $c : m \to \alpha$ does not affect the entry at row $i$ and column $j'$, i.e., $\text{updateCol } M \, j \, c \, i \, j' = M \, i \, j'$.

Matrix.updateRow_apply theorem

[DecidableEq m] {i' : m} : updateRow M i b i' j = if i' = i then b j else M i' j

Full source

theorem updateRow_apply [DecidableEq m] {i' : m} :
    updateRow M i b i' j = if i' = i then b j else M i' j := by
  by_cases h : i' = i
  · rw [h, updateRow_self, if_pos rfl]
  · rw [updateRow_ne h, if_neg h]

Entry-wise Formula for Row Update in a Matrix

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, let $i$ be a row index, and let $b$ be a vector of length $n$. For any row index $i'$ and column index $j$, the entry at row $i'$ and column $j$ of the matrix obtained by updating the $i$-th row of $M$ to $b$ is given by: \[ \text{updateRow } M \, i \, b \, i' \, j = \begin{cases} b \, j & \text{if } i' = i, \\ M \, i' \, j & \text{otherwise.} \end{cases} \]

Matrix.updateCol_apply theorem

[DecidableEq n] {j' : n} : updateCol M j c i j' = if j' = j then c i else M i j'

Full source

theorem updateCol_apply [DecidableEq n] {j' : n} :
    updateCol M j c i j' = if j' = j then c i else M i j' := by
  by_cases h : j' = j
  · rw [h, updateCol_self, if_pos rfl]
  · rw [updateCol_ne h, if_neg h]

Entry-wise Formula for Column Update in a Matrix

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, let $j$ be a column index, and let $c$ be a vector of length $m$. For any row index $i$ and column index $j'$, the entry at row $i$ and column $j'$ of the matrix obtained by updating the $j$-th column of $M$ to $c$ is given by: \[ \text{updateCol } M \, j \, c \, i \, j' = \begin{cases} c_i & \text{if } j' = j, \\ M_{i j'} & \text{otherwise.} \end{cases} \]

Matrix.updateCol_subsingleton theorem

 [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :
  A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0)

Full source

@[simp]
theorem updateCol_subsingleton [Subsingleton n] (A : Matrix m n R) (i : n) (b : m → R) :
    A.updateCol i b = (replicateCol (Fin 1) b).submatrix id (Function.const n 0) := by
  ext x y
  simp [updateCol_apply, Subsingleton.elim i y]

Column Update in Subsingleton Matrix Equals Replicated Column Embedding

Informal description

Let $A$ be an $m \times n$ matrix with entries in a ring $R$, where $n$ is a subsingleton (i.e., has at most one element). For any column index $i$ and vector $b : m \to R$, updating the $i$-th column of $A$ to $b$ results in a matrix that is equal to the matrix obtained by replicating the vector $b$ as a single column (using `Fin 1` as the index type) and then embedding it into the original matrix dimensions via the constant zero function. In other words, $A.\text{updateCol}(i, b) = (\text{replicateCol}(\text{Fin } 1, b)).\text{submatrix}(\text{id}, \text{const}_n 0)$.

Matrix.updateRow_subsingleton theorem

 [Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R) :
  A.updateRow i b = (replicateRow (Fin 1) b).submatrix (Function.const m 0) id

Full source

@[simp]
theorem updateRow_subsingleton [Subsingleton m] (A : Matrix m n R) (i : m) (b : n → R) :
    A.updateRow i b = (replicateRow (Fin 1) b).submatrix (Function.const m 0) id := by
  ext x y
  simp [updateCol_apply, Subsingleton.elim i x]

Row Update in Subsingleton Matrix Equals Replicated Row Embedding

Informal description

Let $A$ be an $m \times n$ matrix with entries in $R$, where $m$ is a subsingleton (i.e., has at most one element). For any row index $i$ and vector $b : n \to R$, updating the $i$-th row of $A$ to $b$ results in a matrix that is equal to the matrix obtained by replicating the vector $b$ as a single row and then embedding it into the original matrix dimensions via the constant zero function. In other words, $A.\text{updateRow}(i, b) = (\text{replicateRow}(\text{Fin } 1, b)).\text{submatrix}(\text{const}_m 0, \text{id})$.

Matrix.map_updateRow theorem

[DecidableEq m] (f : α → β) : map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b)

Full source

theorem map_updateRow [DecidableEq m] (f : α → β) :
    map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b) := by
  ext
  rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
  exact apply_ite f _ _ _

Commutativity of Row Update and Entry-wise Map: $f \circ (\text{updateRow } M \, i \, b) = \text{updateRow } (f \circ M) \, i \, (f \circ b)$

Informal description

Let $M$ be an $m \times n$ matrix with entries in $\alpha$, $i$ a row index, and $b$ a vector in $\alpha^n$. For any function $f : \alpha \to \beta$, applying $f$ entry-wise to the matrix obtained by updating the $i$-th row of $M$ to $b$ is equal to updating the $i$-th row of the matrix $f \circ M$ (where $f$ is applied entry-wise to $M$) to $f \circ b$. In symbols: \[ f \circ (\text{updateRow } M \, i \, b) = \text{updateRow } (f \circ M) \, i \, (f \circ b). \]

Matrix.map_updateCol theorem

[DecidableEq n] (f : α → β) : map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c)

Full source

theorem map_updateCol [DecidableEq n] (f : α → β) :
    map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c) := by
  ext
  rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
  exact apply_ite f _ _ _

Commutativity of Matrix Column Update with Entry-wise Function Application

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, let $j$ be a column index, and let $c$ be a vector of length $m$. For any function $f : \alpha \to \beta$, applying $f$ entry-wise to the matrix obtained by updating the $j$-th column of $M$ to $c$ is equal to updating the $j$-th column of the matrix obtained by applying $f$ entry-wise to $M$ with the vector $f \circ c$. In other words: \[ \text{map } (\text{updateCol } M \, j \, c) \, f = \text{updateCol } (M.\text{map } f) \, j \, (f \circ c) \]

Matrix.updateRow_transpose theorem

[DecidableEq n] : updateRow Mᵀ j c = (updateCol M j c)ᵀ

Full source

theorem updateRow_transpose [DecidableEq n] : updateRow Mᵀ j c = (updateCol M j c)ᵀ := by
  ext
  rw [transpose_apply, updateRow_apply, updateCol_apply]
  rfl

Transpose Commutes with Row/Column Update: $\text{updateRow } M^\top \, j \, c = (\text{updateCol } M \, j \, c)^\top$

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, and let $j$ be a column index and $c$ a vector of length $m$. The operation of updating the $j$-th row of the transpose matrix $M^\top$ to $c$ is equivalent to transposing the matrix obtained by updating the $j$-th column of $M$ to $c$. In other words: \[ \text{updateRow } M^\top \, j \, c = (\text{updateCol } M \, j \, c)^\top. \]

Matrix.updateCol_transpose theorem

[DecidableEq m] : updateCol Mᵀ i b = (updateRow M i b)ᵀ

Full source

theorem updateCol_transpose [DecidableEq m] : updateCol Mᵀ i b = (updateRow M i b)ᵀ := by
  ext
  rw [transpose_apply, updateRow_apply, updateCol_apply]
  rfl

Transpose Commutes with Column and Row Updates: $\text{updateCol } M^\top \, i \, b = (\text{updateRow } M \, i \, b)^\top$

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$, let $i$ be a row index, and let $b$ be a vector of length $n$. Then updating the $i$-th column of the transpose matrix $M^\top$ with the vector $b$ is equal to the transpose of the matrix obtained by updating the $i$-th row of $M$ with $b$. In symbols: \[ \text{updateCol } M^\top \, i \, b = (\text{updateRow } M \, i \, b)^\top. \]

Matrix.updateRow_conjTranspose theorem

[DecidableEq n] [Star α] : updateRow Mᴴ j (star c) = (updateCol M j c)ᴴ

Full source

theorem updateRow_conjTranspose [DecidableEq n] [Star α] :
    updateRow Mᴴ j (star c) = (updateCol M j c)ᴴ := by
  rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose,
    map_updateCol]
  rfl

Conjugate Transpose Commutes with Row/Column Update: $\text{updateRow } M^\mathsf{H} \, j \, \overline{c} = (\text{updateCol } M \, j \, c)^\mathsf{H}$

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$ equipped with a star operation (e.g., complex conjugation), and let $j$ be a column index and $c$ a vector of length $m$. Then updating the $j$-th row of the conjugate transpose matrix $M^\mathsf{H}$ with the conjugate vector $\overline{c}$ is equal to the conjugate transpose of the matrix obtained by updating the $j$-th column of $M$ with $c$. In symbols: \[ \text{updateRow } M^\mathsf{H} \, j \, \overline{c} = (\text{updateCol } M \, j \, c)^\mathsf{H}. \]

Matrix.updateCol_conjTranspose theorem

[DecidableEq m] [Star α] : updateCol Mᴴ i (star b) = (updateRow M i b)ᴴ

Full source

theorem updateCol_conjTranspose [DecidableEq m] [Star α] :
    updateCol Mᴴ i (star b) = (updateRow M i b)ᴴ := by
  rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateCol_transpose,
    map_updateRow]
  rfl

Conjugate Transpose Commutes with Column and Row Updates: $\text{updateCol } M^\mathsf{H} \, i \, (\mathsf{star}\, b) = (\text{updateRow } M \, i \, b)^\mathsf{H}$

Informal description

Let $M$ be an $m \times n$ matrix with entries in a type $\alpha$ equipped with a star operation (e.g., complex conjugation), and let $i$ be a row index. Then updating the $i$-th column of the conjugate transpose matrix $M^\mathsf{H}$ with the vector $\mathsf{star}\, b$ is equal to the conjugate transpose of the matrix obtained by updating the $i$-th row of $M$ with $b$. In symbols: \[ \text{updateCol } M^\mathsf{H} \, i \, (\mathsf{star}\, b) = (\text{updateRow } M \, i \, b)^\mathsf{H}. \]

Matrix.updateRow_eq_self theorem

[DecidableEq m] (A : Matrix m n α) (i : m) : A.updateRow i (A i) = A

Full source

@[simp]
theorem updateRow_eq_self [DecidableEq m] (A : Matrix m n α) (i : m) : A.updateRow i (A i) = A :=
  Function.update_eq_self i A

Matrix Row Update with Original Values Preserves Identity

Informal description

For any matrix $A$ of size $m \times n$ with entries in $\alpha$, and any row index $i \in m$, updating the $i$-th row of $A$ with its own values (i.e., $A_i$) leaves the matrix unchanged: $\text{updateRow } A \, i \, (A i) = A$.

Matrix.updateCol_eq_self theorem

[DecidableEq n] (A : Matrix m n α) (i : n) : (A.updateCol i fun j => A j i) = A

Full source

@[simp]
theorem updateCol_eq_self [DecidableEq n] (A : Matrix m n α) (i : n) :
    (A.updateCol i fun j => A j i) = A :=
  funext fun j => Function.update_eq_self i (A j)

Matrix Column Update with Original Values Preserves Identity

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, and let $i$ be a column index. If we update the $i$-th column of $A$ with the vector formed by the $i$-th entry of each row (i.e., the original column itself), then the resulting matrix is equal to $A$. In other words, $A.\text{updateCol } i \, (\lambda j, A j i) = A$.

Matrix.diagonal_updateCol_single theorem

 [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
  (diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x)

Full source

theorem diagonal_updateCol_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
    (diagonal v).updateCol i (Pi.single i x) = diagonal (Function.update v i x) := by
  ext j k
  obtain rfl | hjk := eq_or_ne j k
  · rw [diagonal_apply_eq]
    obtain rfl | hji := eq_or_ne j i
    · rw [updateCol_self, Pi.single_eq_same, Function.update_self]
    · rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]
  · rw [diagonal_apply_ne _ hjk]
    obtain rfl | hki := eq_or_ne k i
    · rw [updateCol_self, Pi.single_eq_of_ne hjk]
    · rw [updateCol_ne hki, diagonal_apply_ne _ hjk]

Diagonal Matrix Column Update with Single Nonzero Entry

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a type with a zero element, $v : n \to \alpha$ a vector, $i \in n$ an index, and $x \in \alpha$ a value. Then updating the $i$-th column of the diagonal matrix $\text{diagonal } v$ with the vector $\text{Pi.single } i \, x$ (which is zero everywhere except at $i$ where it equals $x$) results in a new diagonal matrix where the $i$-th diagonal entry is updated to $x$ and all other entries remain unchanged. That is, \[ (\text{diagonal } v).\text{updateCol } i \, (\text{Pi.single } i \, x) = \text{diagonal } (\text{Function.update } v \, i \, x). \]

Matrix.diagonal_updateRow_single theorem

 [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
  (diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x)

Full source

theorem diagonal_updateRow_single [DecidableEq n] [Zero α] (v : n → α) (i : n) (x : α) :
    (diagonal v).updateRow i (Pi.single i x) = diagonal (Function.update v i x) := by
  rw [← diagonal_transpose, updateRow_transpose, diagonal_updateCol_single, diagonal_transpose]

Diagonal Matrix Row Update with Single Nonzero Entry

Informal description

Let $n$ be a type with decidable equality, $\alpha$ a type with a zero element, $v : n \to \alpha$ a vector, $i \in n$ an index, and $x \in \alpha$ a value. Then updating the $i$-th row of the diagonal matrix $\text{diagonal } v$ with the vector $\text{Pi.single } i \, x$ (which is zero everywhere except at $i$ where it equals $x$) results in a new diagonal matrix where the $i$-th diagonal entry is updated to $x$ and all other entries remain unchanged. That is, \[ (\text{diagonal } v).\text{updateRow } i \, (\text{Pi.single } i \, x) = \text{diagonal } (\text{Function.update } v \, i \, x). \]

Matrix.updateRow_submatrix_equiv theorem

 [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n) :
  updateRow (A.submatrix e f) i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix e f

Full source

theorem updateRow_submatrix_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l)
    (r : o → α) (e : l ≃ m) (f : o ≃ n) :
    updateRow (A.submatrix e f) i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix e f := by
  ext i' j
  simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]

Commutativity of Row Update and Submatrix via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $i$ be a row index in $l$, $r$ be a vector of length $o$, and $e : l \simeq m$ and $f : o \simeq n$ be bijections. Then updating the $i$-th row of the submatrix $A.\text{submatrix}\, e\, f$ with the vector $r$ is equivalent to first updating the $(e\, i)$-th row of $A$ with the vector $\lambda j, r (f^{-1} j)$, and then taking the submatrix via $e$ and $f$. In other words, the following equality holds: \[ \text{updateRow}\, (A.\text{submatrix}\, e\, f)\, i\, r = (A.\text{updateRow}\, (e\, i)\, (\lambda j, r (f^{-1} j))).\text{submatrix}\, e\, f. \]

Matrix.submatrix_updateRow_equiv theorem

 [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : l ≃ m) (f : o ≃ n) :
  (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) fun i => r (f i)

Full source

theorem submatrix_updateRow_equiv [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m)
    (r : n → α) (e : l ≃ m) (f : o ≃ n) :
    (A.updateRow i r).submatrix e f = updateRow (A.submatrix e f) (e.symm i) fun i => r (f i) :=
  Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateRow_submatrix_equiv A _ _ e f).symm

Commutativity of Submatrix and Row Update via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $i$ be a row index in $m$, $r$ be a vector of length $n$, and $e : l \simeq m$ and $f : o \simeq n$ be bijections. Then taking the submatrix via $e$ and $f$ of the matrix obtained by updating the $i$-th row of $A$ with $r$ is equivalent to updating the $(e^{-1} i)$-th row of the submatrix $A.\text{submatrix}\, e\, f$ with the vector $\lambda k, r (f k)$. In other words, the following equality holds: \[ (A.\text{updateRow}\, i\, r).\text{submatrix}\, e\, f = \text{updateRow}\, (A.\text{submatrix}\, e\, f)\, (e^{-1} i)\, (\lambda k, r (f k)). \]

Matrix.updateCol_submatrix_equiv theorem

 [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n) :
  updateCol (A.submatrix e f) j c = (A.updateCol (f j) fun i => c (e.symm i)).submatrix e f

Full source

theorem updateCol_submatrix_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o)
    (c : l → α) (e : l ≃ m) (f : o ≃ n) : updateCol (A.submatrix e f) j c =
    (A.updateCol (f j) fun i => c (e.symm i)).submatrix e f := by
  simpa only [← transpose_submatrix, updateRow_transpose] using
    congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)

Commutativity of Column Update and Submatrix via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, $j$ be a column index in $o$, $c$ be a vector of length $l$, and $e : l \simeq m$ and $f : o \simeq n$ be bijections. Then updating the $j$-th column of the submatrix $A.\text{submatrix}\, e\, f$ with the vector $c$ is equivalent to first updating the $(f\, j)$-th column of $A$ with the vector $\lambda i, c (e^{-1} i)$, and then taking the submatrix via $e$ and $f$. In other words, the following equality holds: \[ \text{updateCol}\, (A.\text{submatrix}\, e\, f)\, j\, c = (A.\text{updateCol}\, (f\, j)\, (\lambda i, c (e^{-1} i))).\text{submatrix}\, e\, f. \]

Matrix.submatrix_updateCol_equiv theorem

 [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : l ≃ m) (f : o ≃ n) :
  (A.updateCol j c).submatrix e f = updateCol (A.submatrix e f) (f.symm j) fun i => c (e i)

Full source

theorem submatrix_updateCol_equiv [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n)
    (c : m → α) (e : l ≃ m) (f : o ≃ n) : (A.updateCol j c).submatrix e f =
    updateCol (A.submatrix e f) (f.symm j) fun i => c (e i) :=
  Eq.trans (by simp_rw [Equiv.apply_symm_apply]) (updateCol_submatrix_equiv A _ _ e f).symm

Commutativity of Submatrix and Column Update via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $j$ be a column index in $n$, $c$ be a vector of length $m$, and $e : l \simeq m$ and $f : o \simeq n$ be bijections. Then taking the submatrix via $e$ and $f$ of the matrix obtained by updating the $j$-th column of $A$ with $c$ is equivalent to updating the $(f^{-1} j)$-th column of the submatrix $A.\text{submatrix}\, e\, f$ with the vector $\lambda i, c (e i)$. In other words, the following equality holds: \[ (A.\text{updateCol}\, j\, c).\text{submatrix}\, e\, f = \text{updateCol}\, (A.\text{submatrix}\, e\, f)\, (f^{-1} j)\, (\lambda i, c (e i)). \]

Matrix.updateRow_reindex theorem

 [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : m ≃ l) (f : n ≃ o) :
  updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) fun j => r (f j))

Full source

theorem updateRow_reindex [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α)
    (e : m ≃ l) (f : n ≃ o) :
    updateRow (reindex e f A) i r = reindex e f (A.updateRow (e.symm i) fun j => r (f j)) :=
  updateRow_submatrix_equiv _ _ _ _ _

Commutativity of Row Update and Reindexing via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $i$ be a row index in $l$, $r$ be a vector of length $o$, and $e : m \simeq l$ and $f : n \simeq o$ be bijections. Then updating the $i$-th row of the reindexed matrix $\text{reindex}\, e\, f\, A$ with the vector $r$ is equivalent to first updating the $(e^{-1}\, i)$-th row of $A$ with the vector $\lambda j, r (f\, j)$, and then reindexing the resulting matrix via $e$ and $f$. In other words, the following equality holds: \[ \text{updateRow}\, (\text{reindex}\, e\, f\, A)\, i\, r = \text{reindex}\, e\, f\, (A.\text{updateRow}\, (e^{-1}\, i)\, (\lambda j, r (f\, j))). \]

Matrix.reindex_updateRow theorem

 [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α) (e : m ≃ l) (f : n ≃ o) :
  reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) fun i => r (f.symm i)

Full source

theorem reindex_updateRow [DecidableEq l] [DecidableEq m] (A : Matrix m n α) (i : m) (r : n → α)
    (e : m ≃ l) (f : n ≃ o) :
    reindex e f (A.updateRow i r) = updateRow (reindex e f A) (e i) fun i => r (f.symm i) :=
  submatrix_updateRow_equiv _ _ _ _ _

Commutativity of Reindexing and Row Update via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in $\alpha$, $i$ be a row index in $m$, $r$ be a vector of length $n$, and $e : m \simeq l$ and $f : n \simeq o$ be bijections. Then reindexing the matrix obtained by updating the $i$-th row of $A$ with $r$ via $e$ and $f$ is equivalent to updating the $(e\, i)$-th row of the reindexed matrix $\text{reindex}\, e\, f\, A$ with the vector $\lambda k, r (f^{-1} k)$. In other words, the following equality holds: \[ \text{reindex}\, e\, f\, (A.\text{updateRow}\, i\, r) = \text{updateRow}\, (\text{reindex}\, e\, f\, A)\, (e\, i)\, (\lambda k, r (f^{-1} k)). \]

Matrix.updateCol_reindex theorem

 [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : m ≃ l) (f : n ≃ o) :
  updateCol (reindex e f A) j c = reindex e f (A.updateCol (f.symm j) fun i => c (e i))

Full source

theorem updateCol_reindex [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α)
    (e : m ≃ l) (f : n ≃ o) :
    updateCol (reindex e f A) j c = reindex e f (A.updateCol (f.symm j) fun i => c (e i)) :=
  updateCol_submatrix_equiv _ _ _ _ _

Commutativity of Column Update and Reindexing via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, $j$ be a column index in $o$, $c$ be a vector of length $l$, and $e : m \simeq l$ and $f : n \simeq o$ be bijections. Then updating the $j$-th column of the reindexed matrix $\text{reindex}\, e\, f\, A$ with the vector $c$ is equivalent to first updating the $(f^{-1}\, j)$-th column of $A$ with the vector $\lambda i, c (e\, i)$, and then reindexing the resulting matrix via $e$ and $f$. In other words, the following equality holds: \[ \text{updateCol}\, (\text{reindex}\, e\, f\, A)\, j\, c = \text{reindex}\, e\, f\, (A.\text{updateCol}\, (f^{-1}\, j)\, (\lambda i, c (e\, i))). \]

Matrix.reindex_updateCol theorem

 [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α) (e : m ≃ l) (f : n ≃ o) :
  reindex e f (A.updateCol j c) = updateCol (reindex e f A) (f j) fun i => c (e.symm i)

Full source

theorem reindex_updateCol [DecidableEq o] [DecidableEq n] (A : Matrix m n α) (j : n) (c : m → α)
    (e : m ≃ l) (f : n ≃ o) :
    reindex e f (A.updateCol j c) = updateCol (reindex e f A) (f j) fun i => c (e.symm i) :=
  submatrix_updateCol_equiv _ _ _ _ _

Commutativity of Reindexing and Column Update via Bijections

Informal description

Let $A$ be an $m \times n$ matrix with entries in a type $\alpha$, $j$ be a column index in $n$, $c$ be a vector of length $m$, and $e : m \simeq l$ and $f : n \simeq o$ be bijections. Then reindexing the matrix obtained by updating the $j$-th column of $A$ with $c$ via $e$ and $f$ is equivalent to updating the $(f\, j)$-th column of the reindexed matrix $\text{reindex}\, e\, f\, A$ with the vector $\lambda i, c (e^{-1} i)$. In other words, the following equality holds: \[ \text{reindex}\, e\, f\, (A.\text{updateCol}\, j\, c) = \text{updateCol}\, (\text{reindex}\, e\, f\, A)\, (f\, j)\, (\lambda i, c (e^{-1} i)). \]

Main definitions