fact: Definition delta_mx i0 j0 := \matrix_(i < m, j < n) (if ((i == i0) && (j == j0)) then 1 else 0).
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype finfun bigops ssralg groups perm zmodp morphisms Ring RingClass bigopsClass Setoid Morphisms