English
Let M be an n-by-n matrix over a ring α (with 1) and let d be an integer. The matrix with all diagonal entries equal to the integer d (viewed inside α) has the property that M^T equals this diagonal matrix if and only if M equals this diagonal matrix.
Русский
Пусть M — матрица размером n×n над кольцом α (с единицей), а d — целое число. Диагональная матрица, у которой на диагонали стоят все элементы d в α, удовлетворяет: M^T = diag(d) тогда и только тогда, когда M = diag(d).
LaTeX
$$$M^{\top} = \operatorname{diag}(d) \iff M = \operatorname{diag}(d),$$$
Lean4
@[simp]
theorem transpose_eq_intCast [DecidableEq n] [AddGroupWithOne α] {M : Matrix n n α} {d : ℤ} : Mᵀ = d ↔ M = d :=
transpose_eq_diagonal
