transpose_submatrix — Mathlib

English

Taking a submatrix and then transposing is the same as transposing first and then taking the corresponding submatrix: (A.submatrix r c)ᵀ = Aᵀ.submatrix c r.

Русский

Сначала берём подматрицу, затем транспонируем, что эквивалентно транспонированию и взятию соответствующей подматрицы: (A.submatrix r c)ᵀ = Aᵀ.submatrix c r.

LaTeX

$$$ (A.submatrix\ r\ c)^T = A^T.submatrix\ c\ r $$$

Lean4

@[simp]
theorem transpose_submatrix (A : Matrix m n α) (r : l → m) (c : o → n) : (A.submatrix r c)ᵀ = Aᵀ.submatrix c r :=
  ext fun _ _ => rfl

Похожие утверждения