instFinite

Mathlib.Analysis.CStarAlgebra.CStarMatrix

URI: https://scilib.ai/kg/mathlib#CStarMatrix.instFinite

English

If m,n are finite and α is finite, then CStarMatrix m n α is finite.

Русский

Если m и n конечны, а α конечно, то CStarMatrix m n α конечно.

LaTeX

$$$[Finite m] [Finite n] (\alpha) [Finite \alpha] : Finite (CStarMatrix m n α)$$$

Lean4

instance {n m} [Finite m] [Finite n] (α) [Finite α] : Finite (CStarMatrix m n α) :=
  inferInstanceAs (Finite (m → n → α))

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

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

Разделы

Аффилиация

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