submatrix_mul_transpose_submatrix

English

Let m,n be finite, α a commutative semiring with addition. For a bijection e: m ≃ n and M ∈ M_{m×n}(α), M.submatrix id e times Mᵀ.submatrix e id equals M Mᵀ.

Русский

Пусть e: m ≃ n является биекцией; для матрицы M размерности m×n имеет место равенство: M.submatrix id e · Mᵀ.submatrix e id = M Mᵀ.

LaTeX

$$$\\text{Let } e: M \\simeq N,\\; M ∈ M_{m\\times n}(α).\\quad M_{sub}^{id,e} \\cdot M^{\\top}_{sub}^{e,id} = M \\cdot M^{\\top}.$$$

Lean4

theorem submatrix_mul_transpose_submatrix [Fintype m] [Fintype n] [AddCommMonoid α] [Mul α] (e : m ≃ n)
    (M : Matrix m n α) : M.submatrix id e * Mᵀ.submatrix e id = M * Mᵀ := by rw [submatrix_mul_equiv, submatrix_id_id]

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