unique

Mathlib.LinearAlgebra.Matrix.Defs

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

English

If α is Unique, then Matrix m n α is Unique.

Русский

Если α уникальна, то Matrix m n α также уникальна.

LaTeX

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

Lean4

instance unique [Unique α] : Unique (Matrix m n α) :=
  Pi.unique

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

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

Разделы

Аффилиация

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