ofNat

Mathlib.LinearAlgebra.Matrix.PosDef

URI: https://scilib.ai/kg/mathlib#Matrix.PosDef.ofNat

← MathLib Explorer

English

There is a PosDef matrix corresponding to natural numbers via embedding.

Русский

Существует PosDef матрица, соответствующая натуральному числу через вложение.

LaTeX

$$PosDef( ofNat(d) )$$

Lean4

protected theorem ofNat [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] (d : ℕ) [d.AtLeastTwo] :
    PosDef (ofNat(d) : Matrix n n R) :=
  .natCast d (NeZero.ne _)

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

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

Разделы

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

Аффилиация

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