decidableEq — Mathlib

English

If α has decidable equality and m,n are finite, then the matrix set M_{m,n}(α) has a decidable equality.

Русский

Если α имеет разрешимое равенство, и размеры m,n конечны, то множество матриц M_{m,n}(α) имеет разрешимое равенство.

LaTeX

$$$\\forall m,n,\\ (DecidableEq\\ α)\\to (Fintype m)\\to (Fintype n)\\to DecidableEq (Matrix\\ m\\ n\\ α)$$$

Lean4

instance decidableEq [DecidableEq α] [Fintype m] [Fintype n] : DecidableEq (Matrix m n α) :=
  Fintype.decidablePiFintype

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