conjTranspose_ofNat

Mathlib.LinearAlgebra.Matrix.ConjTranspose

URI: https://scilib.ai/kg/mathlib#Matrix.conjTranspose_ofNat

← MathLib Explorer

English

For Nat d with at least two, conjTranspose(ofNat d) = ofNat d.

Русский

Для Nat d с хотя бы двумя, conjTranspose(ofNat d) = ofNat d.

LaTeX

$$$\operatorname{conjTranspose}(\operatorname{ofNat}(d)) = \operatorname{ofNat}(d)$$$

Lean4

@[simp]
theorem conjTranspose_ofNat [DecidableEq n] [NonAssocSemiring α] [StarRing α] (d : ℕ) [d.AtLeastTwo] :
    (ofNat(d) : Matrix n n α)ᴴ = OfNat.ofNat d :=
  conjTranspose_natCast _

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru