instDecidableEq

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

English

If A has decidable equality and m,n are finite, then CStarMatrix m n A has decidable equality.

Русский

Если A имеет разрешимое равенство и m,n конечны, то CStarMatrix m n A имеетDecidableEq.

LaTeX

$$$[DecidableEq A] [Fintype m] [Fintype n] : DecidableEq (CStarMatrix m n A)$$$

Lean4

instance instDecidableEq [DecidableEq A] [Fintype m] [Fintype n] : DecidableEq (CStarMatrix m n A) :=
  Fintype.decidablePiFintype

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

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

Разделы

Аффилиация

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