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]