instFintypeOfDecidableEq — Mathlib

English

If m,n are finite and α is finite, then the set of matrices CStarMatrix m n α is finite.

Русский

Если m и n конечны, а α конечно, то множество CStarMatrix m n α конечно.

LaTeX

$$$[Finite m] [Finite n] (\alpha) [Finite \alpha] : Finite (CStarMatrix m n α)$$$

Lean4

instance {n m} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α) [Fintype α] : Fintype (CStarMatrix m n α) :=
  inferInstanceAs (Fintype (m → n → α))

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