Matrices over a countable type, with finitely many entries, are countable

Matrix m n α is a semireducible definition rather than an abbreviation, so instance synthesis does not see through it to the underlying m → n → α: Countable (m → n → α) resolves and Countable (Matrix m n α) does not. This is the same reason Mathlib states the Matrix algebraic instances explicitly rather than inheriting them from Pi.

Main results

• Matrix.instCountable: Matrix m n α is countable for finite index types and countable entries.

instance Matrix.instCountable {m : Type u_1} {n : Type u_2} {α : Type u_3} [Finite m] [Finite n] [Countable α] : Countable (Matrix m n α)

Matrices indexed by finite types, with entries in a countable type, form a countable type.

Stated because Matrix does not unfold during instance synthesis; the proof is just the corresponding fact for its underlying function type.