subsingleton_of_empty_right

Mathlib.LinearAlgebra.Matrix.Defs

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

English

If n is empty, then the matrix space over α is a singleton.

Русский

Если множество справа пустое, пространство матриц над α является единственным элементом.

LaTeX

$$$ IsEmpty(n) \\Rightarrow Subsingleton(Matrix(m,n,\\alpha)) $$$

Lean4

instance subsingleton_of_empty_right [IsEmpty n] : Subsingleton (Matrix m n α) :=
  ⟨fun M N => by
    ext i j
    exact isEmptyElim j⟩

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

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

Разделы

Аффилиация

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