transpose_intCast — Mathlib

English

For any integer d, the transpose of its matrix embedding equals the same embedding: (d : Matrix)^{T} = d.

Русский

Для любого целого числа d транспонированная матрица, полученная через целочисленное приведение, равна самой матрице: (d : Matrix)^{T} = d.

LaTeX

$$$\bigl(d : \mathrm{Matrix}\ n\ n\ α\bigr)^{\top} = d$$$

Lean4

@[simp]
theorem transpose_intCast [DecidableEq n] [AddGroupWithOne α] (d : ℤ) : (d : Matrix n n α)ᵀ = d :=
  diagonal_transpose _

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