transpose_ofNat — Mathlib

English

If d is a natural, then the matrix of d under the OfNat embedding is symmetric: ofNat(d)^{T} = OfNat(d).

Русский

Если d — натуральное число, то матрица, полученная через OfNat(d), симметрична: OfNat(d)^{T} = OfNat(d).

LaTeX

$$$\bigl(\mathrm{ofNat}(d)\bigr)^{\top} = \mathrm{OfNat}(d)$$$

Lean4

@[simp]
theorem transpose_ofNat [DecidableEq n] [AddMonoidWithOne α] (d : ℕ) [d.AtLeastTwo] :
    (ofNat(d) : Matrix n n α)ᵀ = OfNat.ofNat d :=
  transpose_natCast _

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