def Hex.Matrix.fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (A₁₁ : Matrix R n₁ m₁) (A₁₂ : Matrix R n₁ m₂) (A₂₁ : Matrix R n₂ m₁) (A₂₂ : Matrix R n₂ m₂) : Matrix R (n₁ + n₂) (m₁ + m₂)

Assemble a matrix from four blocks, laid out as [[A₁₁, A₁₂], [A₂₁, A₂₂]]. The result is (n₁ + n₂) × (m₁ + m₂); Fin.addCases routes each row/column index to the block it lands in.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Hex.Matrix.getElem_fromBlocks₁₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₁) (j : Fin m₁) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)[Fin.castAdd n₂ i][Fin.castAdd m₂ j] = A₁₁[i][j]

Top-left block entry of fromBlocks.

@[simp]

theorem Hex.Matrix.getElem_fromBlocks₁₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₁) (j : Fin m₂) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)[Fin.castAdd n₂ i][Fin.natAdd m₁ j] = A₁₂[i][j]

Top-right block entry of fromBlocks.

@[simp]

theorem Hex.Matrix.getElem_fromBlocks₂₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₂) (j : Fin m₁) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)[Fin.natAdd n₁ i][Fin.castAdd m₂ j] = A₂₁[i][j]

Bottom-left block entry of fromBlocks.

@[simp]

theorem Hex.Matrix.getElem_fromBlocks₂₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₂) (j : Fin m₂) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂)[Fin.natAdd n₁ i][Fin.natAdd m₁ j] = A₂₂[i][j]

Bottom-right block entry of fromBlocks.

def Hex.Matrix.toBlocks₁₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) : Matrix R n₁ m₁

Extract the top-left n₁ × m₁ block.

Equations

• M.toBlocks₁₁ = Hex.Matrix.ofFn fun (i : Fin n₁) (j : Fin m₁) => M[(Fin.castAdd n₂ i, Fin.castAdd m₂ j)]

def Hex.Matrix.toBlocks₁₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) : Matrix R n₁ m₂

Extract the top-right n₁ × m₂ block.

Equations

• M.toBlocks₁₂ = Hex.Matrix.ofFn fun (i : Fin n₁) (j : Fin m₂) => M[(Fin.castAdd n₂ i, Fin.natAdd m₁ j)]

def Hex.Matrix.toBlocks₂₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) : Matrix R n₂ m₁

Extract the bottom-left n₂ × m₁ block.

Equations

• M.toBlocks₂₁ = Hex.Matrix.ofFn fun (i : Fin n₂) (j : Fin m₁) => M[(Fin.natAdd n₁ i, Fin.castAdd m₂ j)]

def Hex.Matrix.toBlocks₂₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) : Matrix R n₂ m₂

Extract the bottom-right n₂ × m₂ block.

Equations

• M.toBlocks₂₂ = Hex.Matrix.ofFn fun (i : Fin n₂) (j : Fin m₂) => M[(Fin.natAdd n₁ i, Fin.natAdd m₁ j)]

@[simp]

theorem Hex.Matrix.getElem_toBlocks₁₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) (i : Fin n₁) (j : Fin m₁) : M.toBlocks₁₁[i][j] = M[Fin.castAdd n₂ i][Fin.castAdd m₂ j]

Entry of the top-left extractor.

@[simp]

theorem Hex.Matrix.getElem_toBlocks₁₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) (i : Fin n₁) (j : Fin m₂) : M.toBlocks₁₂[i][j] = M[Fin.castAdd n₂ i][Fin.natAdd m₁ j]

Entry of the top-right extractor.

@[simp]

theorem Hex.Matrix.getElem_toBlocks₂₁ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) (i : Fin n₂) (j : Fin m₁) : M.toBlocks₂₁[i][j] = M[Fin.natAdd n₁ i][Fin.castAdd m₂ j]

Entry of the bottom-left extractor.

@[simp]

theorem Hex.Matrix.getElem_toBlocks₂₂ {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) (i : Fin n₂) (j : Fin m₂) : M.toBlocks₂₂[i][j] = M[Fin.natAdd n₁ i][Fin.natAdd m₁ j]

Entry of the bottom-right extractor.

@[simp]

theorem Hex.Matrix.toBlocks₁₁_fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).toBlocks₁₁ = A₁₁

Extracting the top-left quadrant of an assembly returns the block.

@[simp]

theorem Hex.Matrix.toBlocks₁₂_fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).toBlocks₁₂ = A₁₂

Extracting the top-right quadrant of an assembly returns the block.

@[simp]

theorem Hex.Matrix.toBlocks₂₁_fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).toBlocks₂₁ = A₂₁

Extracting the bottom-left quadrant of an assembly returns the block.

@[simp]

theorem Hex.Matrix.toBlocks₂₂_fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).toBlocks₂₂ = A₂₂

Extracting the bottom-right quadrant of an assembly returns the block.

@[simp]

theorem Hex.Matrix.fromBlocks_toBlocks {R : Type u} {n₁ n₂ m₁ m₂ : Nat} (M : Matrix R (n₁ + n₂) (m₁ + m₂)) : M.toBlocks₁₁.fromBlocks M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M

Reassembling a matrix from its four extracted quadrants returns the matrix.

@[simp]

theorem Hex.Matrix.row_fromBlocks_castAdd {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₁) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).row (Fin.castAdd n₂ i) = A₁₁.row i ++ A₁₂.row i

Row Fin.castAdd n₂ i of an assembly is the concatenation of the two top-block rows.

@[simp]

theorem Hex.Matrix.row_fromBlocks_natAdd {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (i : Fin n₂) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).row (Fin.natAdd n₁ i) = A₂₁.row i ++ A₂₂.row i

Row Fin.natAdd n₁ i of an assembly is the concatenation of the two bottom-block rows.

@[simp]

theorem Hex.Matrix.col_fromBlocks_castAdd {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (j : Fin m₁) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).col (Fin.castAdd m₂ j) = A₁₁.col j ++ A₂₁.col j

Column Fin.castAdd m₂ j of an assembly is the concatenation of the two left-block columns.

@[simp]

theorem Hex.Matrix.col_fromBlocks_natAdd {R : Type u} {n₁ n₂ m₁ m₂ : Nat} {A₁₁ : Matrix R n₁ m₁} {A₁₂ : Matrix R n₁ m₂} {A₂₁ : Matrix R n₂ m₁} {A₂₂ : Matrix R n₂ m₂} (j : Fin m₂) : (A₁₁.fromBlocks A₁₂ A₂₁ A₂₂).col (Fin.natAdd m₁ j) = A₁₂.col j ++ A₂₂.col j

Column Fin.natAdd m₁ j of an assembly is the concatenation of the two right-block columns.

theorem Hex.Matrix.fromBlocks_mul_fromBlocks {R : Type u} {n₁ n₂ m₁ m₂ k₁ k₂ : Nat} [Lean.Grind.Ring R] (A₁₁ : Matrix R n₁ m₁) (A₁₂ : Matrix R n₁ m₂) (A₂₁ : Matrix R n₂ m₁) (A₂₂ : Matrix R n₂ m₂) (B₁₁ : Matrix R m₁ k₁) (B₁₂ : Matrix R m₁ k₂) (B₂₁ : Matrix R m₂ k₁) (B₂₂ : Matrix R m₂ k₂) : A₁₁.fromBlocks A₁₂ A₂₁ A₂₂ * B₁₁.fromBlocks B₁₂ B₂₁ B₂₂ = (A₁₁ * B₁₁ + A₁₂ * B₂₁).fromBlocks (A₁₁ * B₁₂ + A₁₂ * B₂₂) (A₂₁ * B₁₁ + A₂₂ * B₂₁) (A₂₁ * B₁₂ + A₂₂ * B₂₂)

Block decomposition of matrix multiplication. The product of two 2×2 block matrices is the assembly of the four quadrant products.