transpose_natCast — Mathlib

English

For any natural 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_natCast [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) : (d : Matrix n n α)ᵀ = d :=
  diagonal_transpose _

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