nonempty

Mathlib.LinearAlgebra.Matrix.Defs

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

English

If m and n are Nonempty and α is Nontrivial, then Matrix m n α is Nontrivial.

Русский

Если области m и n непусты, а α ненульва, то Matrix m n α ненулевая.

LaTeX

$$$ [Nonempty\;m] [Nonempty\;n] [Nontrivial\;α] \Rightarrow Nontrivial\; (Matrix\; m\; n\; α) $$$

Lean4

instance nonempty [Nonempty m] [Nonempty n] [Nontrivial α] : Nontrivial (Matrix m n α) :=
  Function.nontrivial

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

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

Разделы

Аффилиация

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