Error in definition of semisimple finite rings

[fredrik-bakke]

The definition in the library of a semisimple finite ring states that it is a ring that is merely equivalent to a finite product of finite fields, but the formalization only states that it is merely homomorphic to one.