feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add the induced monoid equivalence from a ring hom. on GL and the equivalence between GL n (Π i, R i) ≃* Π i, GL n (R i)

feat(LinearAlgebra/Matrix/GeneralLinearGroup/Defs): add the induced monoid equivalence from a ring hom. on GL and the equivalence between GL n (Π i, R i) ≃* Π i, GL n (R i) #338289