instFinite

Mathlib.Data.Matrix.Basic

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

English

If m,n,α are finite, then Matrix m n α is finite; more generally Finite m × n α.

Русский

Если m,n, α конечны, то Matrix m n α конечно, аналогично Finite множества элементов в виде матриц.

LaTeX

$$$\\text{Finite}(Matrix\\ m\\ n\\ α)$$$

Lean4

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

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

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

Разделы

Аффилиация

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