instNontrivial

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

If m and n are nonempty and A is nontrivial, then CStarMatrix m n A is nontrivial.

Русский

Если m, n непустые и A ненулевой, то CStarMatrix m n A ненулевой.

LaTeX

$$[Nonempty m] [Nonempty n] [Nontrivial A] : Nontrivial (CStarMatrix m n A)$$

Lean4

instance instNontrivial [Nonempty m] [Nonempty n] [Nontrivial A] : Nontrivial (CStarMatrix m n A) :=
  Function.nontrivial

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

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

Разделы

Аффилиация

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