charmatrix_transpose — Mathlib

English

For any square matrix M over a commutative ring, the characteristic matrix commutes with transpose: the characteristic matrix of M transposed equals the transpose of the characteristic matrix of M.

Русский

Для любой квадратной матрицы M над коммутативной кольцом характеристическая матрица коммутирует с операцией транспонирования: charmatrix(M^T) = charmatrix(M)^T.

LaTeX

$$$\operatorname{charmatrix}(M^{\top}) = \left(\operatorname{charmatrix}(M)\right)^{\top}$$$

Lean4

@[simp]
theorem charmatrix_transpose (M : Matrix n n R) : (Mᵀ).charmatrix = M.charmatrixᵀ := by simp [charmatrix, transpose_map]

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